Too much ghostification?
In the following example, the ghostification that is introduced by line 16, is expanded to line 12, which results in a compilation error.
The example code works fine when f
is non-recursive, when the ghost
keyword is removed from line 16, or when an ; ()
is added after line 16.
$ cat test.mlw
module Test
use option.Option
let ref x = ()
exception E
type t = A | B
let rec f (t: t) diverges raises { E -> true } =
match t with
| A ->
x <- () (* Line 12 *)
| B ->
try
f t;
ghost () (* Line 16 *)
with E ->
raise E
end
end
end
$ why3 extract --modular -D ocaml64 -L . test.Test -o /tmp
File "./test.mlw", line 12, characters 6-13:
This expression makes a ghost modification in the non-ghost variable x