mutexEvents: Do not emit refines of form &a=&a

goblint · Mar 28, 2024 · 96e7b37 · 96e7b37
1 parent 0c72199
commit 96e7b37
Showing 1 changed file with 6 additions and 2 deletions.
diff --git a/src/analyses/mutexEventsAnalysis.ml b/src/analyses/mutexEventsAnalysis.ml
@@ -23,8 +23,12 @@ struct
   let lock ctx rw may_fail nonzero_return_when_aquired a lv_opt arg =
     let compute_refine_split (e:Mutexes.elt) = match e with
       | Addr a ->
-        let e' = BinOp(Eq, arg, AddrOf ((PreValueDomain.Mval.to_cil a)), intType) in
-        [Events.SplitBranch  (e',true)]
+        let arg_e = AddrOf (PreValueDomain.Mval.to_cil a) in
+        if not (CilType.Exp.equal arg arg_e) then
+          let e' = BinOp(Eq, arg, AddrOf (PreValueDomain.Mval.to_cil a), intType) in
+          [Events.SplitBranch  (e',true)]
+        else
+          []
       | _ -> []
     in
     match lv_opt with