Skip to content

Commit 51676de

Browse files
committed
Add exp.volatiles_are_top back to none privatization
1 parent c14fdf3 commit 51676de

File tree

1 file changed

+6
-0
lines changed

1 file changed

+6
-0
lines changed

src/analyses/basePriv.ml

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -121,6 +121,12 @@ struct
121121
getg x
122122

123123
let write_global ?(invariant=false) (ask: Queries.ask) getg sideg (st: BaseComponents (D).t) x v =
124+
let v = (* Copied from MainFunctor.update_variable *)
125+
if get_bool "exp.volatiles_are_top" && is_always_unknown x then (* TODO: why don't other privatizations do this? why in write_global, not read_global? why not in base directly? why not in other value analyses? *)
126+
VD.top ()
127+
else
128+
v
129+
in
124130
if not invariant then
125131
sideg x v;
126132
st

0 commit comments

Comments
 (0)