protection-atomic: Properly handle unlock of atomicity mutex

Author: michael-schwarz

src/analyses/basePriv.ml

@@ -980,7 +980,7 @@ struct
     let atomic = Param.handle_atomic && LockDomain.MustLock.equal m (LockDomain.MustLock.of_var LibraryFunctions.verifier_atomic_var) in
     (* TODO: what about G_m globals in cpa that weren't actually written? *)
     CPA.fold (fun x v (st: BaseComponents (D).t) ->
-        if is_protected_by ask m x then ( (* is_in_Gm *)
+        if (atomic && is_global ask x && not (VD.is_immediate_type x.vtype)) || is_protected_by ask m x then ( (* is_in_Gm *)
           (* Only apply sides for values that were actually written to globals!
              This excludes invariants inferred through guards. *)
           begin match D.precise_side x v st.priv with

tests/regression/13-privatized/97-atomic-p.c

@@ -0,0 +1,27 @@
+// PARAM: --disable warn.race --enable ana.sv-comp.functions --set ana.path_sens[+] threadflag --set lib.activated[+] sv-comp --set ana.base.privatization protection-atomic
+#include<pthread.h>
+#include<stdlib.h>
+#include<goblint.h>
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int g;
+
+void fun() {
+    g = 1;
+}
+
+int main(void) {
+    pthread_t thread;
+    pthread_create(&thread, NULL, (void*)fun, NULL);
+
+    __VERIFIER_atomic_begin();
+    g = 1;
+    __VERIFIER_atomic_end();
+
+    g = 5;
+    __goblint_check(g <= 1); //UNKNOWN!
+
+
+    return 0;
+}