GitLab

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