Fix relational mutex-meet-atomic publishing top with empty environment

goblint · May 3, 2024 · 1dcb3c9 · 1dcb3c9
1 parent 52fce5a
commit 1dcb3c9
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
@@ -607,7 +607,10 @@ struct
         )
       in
       (* Unprotected invariant is one big relation. *)
-      sideg (V.mutex atomic_mutex) rel_side;
+      (* If no globals are contained here, none need to be published *)
+      (* https://github.com/goblint/analyzer/pull/1354 *)
+      if RD.vars rel_side <> [] then
+        sideg (V.mutex atomic_mutex) rel_side;
       let rel_local =
         let newly_unprot var = match AV.find_metadata var with
           | Some (Global g) -> is_unprotected_without ask g atomic_mutex