Skip to content

Commit

Permalink
set: For non-definite AD, join over **all** components not just cpa
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
michael-schwarz committed May 13, 2024
1 parent 44eb176 commit d033d7d
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/analyses/base.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1723,7 +1723,7 @@ struct
(* if M.tracing then M.tracel "set" ~var:firstvar "new state1 %a" CPA.pretty nst; *)
(* If the address was definite, then we just return it. If the address
* was ambiguous, we have to join it with the initial state. *)
let nst = if AD.cardinal lval > 1 then { nst with cpa = CPA.join st.cpa nst.cpa } else nst in
let nst = if AD.cardinal lval > 1 then D.join st nst else nst in
(* if M.tracing then M.tracel "set" ~var:firstvar "new state2 %a" CPA.pretty nst; *)
nst
with
Expand Down

0 comments on commit d033d7d

Please sign in to comment.