Modify Library Function Specification for assert to not dereference its argument

src/analyses/libraryFunctions.ml

@@ -15,7 +15,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("realloc", special [__ "ptr" [r; f]; __ "size" []] @@ fun ptr size -> Realloc { ptr; size });
     ("abort", special [] Abort);
     ("exit", special [drop "exit_code" []] Abort);
-    ("assert", special [__ "cond" [r]] @@ fun cond -> Assert cond);
+    ("assert", special [__ "cond" []] @@ fun cond -> Assert cond);
   ]
 
 (** C POSIX library functions.
@@ -620,4 +620,4 @@ let find f =
     | Some old_accesses ->
       LibraryDesc.of_old old_accesses (classify name)
     | None ->
-      unknown_desc ~f name
+      unknown_desc ~f name

src/domains/events.ml

@@ -18,4 +18,4 @@ let pretty () = function
   | SplitBranch (exp, tv) -> dprintf "SplitBranch (%a, %B)" d_exp exp tv
   | AssignSpawnedThread (lval, tid) -> dprintf "AssignSpawnedThread (%a, %a)" d_lval lval ThreadIdDomain.Thread.pretty tid
   | Access {var_opt; kind} -> dprintf "Access {var_opt=%a, kind=%a}" (docOpt (CilType.Varinfo.pretty ())) var_opt AccessKind.pretty kind
-  | Assign {lval; exp} -> dprintf "Assugn {lval=%a, exp=%a}" CilType.Lval.pretty lval CilType.Exp.pretty exp
+  | Assign {lval; exp} -> dprintf "Assign {lval=%a, exp=%a}" CilType.Lval.pretty lval CilType.Exp.pretty exp

tests/regression/02-base/86-spurious.c

@@ -0,0 +1,26 @@
+#include<pthread.h>
+#include<assert.h>
+int counter = 0;
+pthread_mutex_t lock1;
+
+void* producer(void* param) {
+    pthread_mutex_lock(&lock1);
+    counter = 0;
+    pthread_mutex_unlock(&lock1);
+}
+
+void* consumer(void* param) {
+    pthread_mutex_lock(&lock1);
+    int bla = counter >= 0;
+    // This should not produce a warning about the privatization being unsound
+    assert(counter >= 0);
+    pthread_mutex_unlock(&lock1);
+}
+
+
+int main() {
+    pthread_t thread;
+    pthread_t thread2;
+    pthread_create(&thread,NULL,producer,NULL);
+    pthread_create(&thread2,NULL,consumer,NULL);
+}