On 10/09/2016 22:58, Per Lindgren wrote:
> Hi Folks.
>
> I’ve observed an obstacle to the code extraction of “let” functions with
> ghost parameters. In cases the generated function code drops ghost
> parameters, while the corresponding calls, do not (leading to compilation
> error later on the OCaml side).
More generally, ocaml extraction is awfully broken with respect to ghost
arguments. Consider the following .mlw code:
module Bug
use import ref.Ref
val z:ref int
let g () (ghost x y:unit): int = !z
let f () =
z := 0;
let t = g () () in
z := 1;
let u = t () in
assert { u = 1 }
end
And the extraction gives:
let f (us: unit) =
begin
let o = Why3__BigInt.zero in
Pervasives.(:=) z o;
let o = () in
let t = g o o1 in (* BUG: no o1 in scope *)
begin
let o2 = Why3__BigInt.one in
Pervasives.(:=) z o2;
let u = t o2 in (* BUG: o2 is an int, not a unit *)
()
end
end
Best regards,
Guillaume
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
http://lists.gforge.inria.fr/mailman/listinfo/why3-club
