From 96e7b37a2682c0dab80f17d6ffdede7d8831b6dc Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 28 Mar 2024 14:40:24 +0100 Subject: [PATCH] mutexEvents: Do not emit refines of form `&a=&a` --- src/analyses/mutexEventsAnalysis.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/analyses/mutexEventsAnalysis.ml b/src/analyses/mutexEventsAnalysis.ml index 7f544b0ffd..a8ae198e14 100644 --- 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