From 1dcb3c9d55c52f57a13004660539f97df41002ac Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 3 May 2024 13:27:05 +0300 Subject: [PATCH] Fix relational mutex-meet-atomic publishing top with empty environment --- src/analyses/apron/relationPriv.apron.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index 66548c117c..1a91b4d39a 100644 --- 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