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