Add ddverify mutex functions to LibraryFunctions

Author: sim642

src/analyses/libraryFunctions.ml

@@ -60,6 +60,7 @@ let classify' fn exps =
       | _ -> M.warn "Assert argument mismatch!"; `Unknown fn
     end
   | "_spin_trylock" | "spin_trylock" | "mutex_trylock" | "_spin_trylock_irqsave"
+  | "down_trylock"
     -> `Lock(true, true, true)
   | "pthread_mutex_trylock" | "pthread_rwlock_trywrlock"
     -> `Lock (true, true, false)
@@ -82,6 +83,7 @@ let classify' fn exps =
   | "_spin_unlock" | "spin_unlock" | "_spin_unlock_irqrestore" | "_spin_unlock_bh" | "_raw_spin_unlock_bh"
   | "mutex_unlock" | "ReleaseResource" | "_write_unlock" | "_read_unlock" | "_raw_spin_unlock_irqrestore"
   | "pthread_mutex_unlock" | "__pthread_mutex_unlock" | "spin_unlock_irqrestore" | "up_read" | "up_write"
+  | "up"
     -> `Unlock
   | x -> `Unknown x
 
@@ -476,6 +478,15 @@ let invalidate_actions = [
     "isatty", readsAll;
     "setpriority", readsAll;
     "getpriority", readsAll;
+    (* ddverify *)
+    "spin_lock_init", readsAll;
+    "spin_lock", readsAll;
+    "spin_unlock", readsAll;
+    "spin_unlock_irqrestore", readsAll;
+    "spin_lock_irqsave", readsAll;
+    "sema_init", readsAll;
+    "down_trylock", readsAll;
+    "up", readsAll;
   ]
 
 (* used by get_invalidate_action to make sure