Incorrect detection of effect interference during extraction
Interference is incorrectly detected by function Compile.no_reads_writes_conflict
. Its body should presumably make use of Vc.pvs_affected
. Testcase:
use ref.Ref, mach.int.Int63
type t = {a: unit; b: ref int63}
let f () ensures { result = 1 } =
let x = { a = (); b = ref 1 } in
x.b.contents <- (let () = x.b.contents <- 0 in x.b.contents) + x.b.contents;
x.b.contents
We can prove that the result of the WhyML function is 1, yet the extracted function returns 0.
$ bin/why3 prove foo.mlw -P alt-ergo
foo.mlw Top VC f: Valid (0.00s, 89 steps)
$ (bin/why3 extract -D ocaml64 foo.mlw; echo 'let () = Printf.printf "%d\n" (f ())') | ocaml -stdin
0