Skip to content

Commit cd79564

Browse files
set: For non-definite AD, join over **all** components not just cpa
Earlier `priv` was not joined over, which lead to unsound results #1457. On top, this also considers `dep` and `weak`. While not strictly necessary to pass tests, this also seems to be the right thing here.
1 parent dc0c3e3 commit cd79564

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/analyses/base.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1738,7 +1738,7 @@ struct
17381738
(* if M.tracing then M.tracel "set" ~var:firstvar "new state1 %a" CPA.pretty nst; *)
17391739
(* If the address was definite, then we just return it. If the address
17401740
* was ambiguous, we have to join it with the initial state. *)
1741-
let nst = if AD.cardinal lval > 1 then { nst with cpa = CPA.join st.cpa nst.cpa } else nst in
1741+
let nst = if AD.cardinal lval > 1 then D.join st nst else nst in
17421742
(* if M.tracing then M.tracel "set" ~var:firstvar "new state2 %a" CPA.pretty nst; *)
17431743
nst
17441744
with

0 commit comments

Comments
 (0)