Commit 2aa32944 authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: fix alias detection

parent fdb529ac
module Bad
use import int.Int
use import ref.Ref
let f (x y : ref int) : unit =
{ !x = !y }
x := !x + 1
{ !x = !y + 1 }
let g () : unit =
let r = ref 0 in
f r r;
absurd
end
......@@ -663,7 +663,7 @@ let eff_full_inst s e =
let wr = Sreg.union e.eff_writes wr in
let wr = Sreg.union e.eff_ghostw wr in
(* read-only regions in e *)
let ro = Sreg.diff (Sreg.union e.eff_reads e.eff_ghostr) wr in
let ro = Sreg.diff (Mreg.map (Util.const ()) s) wr in
(* all modified or reset regions are instantiated into distinct regions *)
let add_affected r acc =
let r = Mreg.find r s in Sreg.add_new (IllegalAlias r) r acc in
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment