non val logic symbols should not be usable in programs
In the following code
type t
constant a : t
val function f t : int
use ref.Ref
let test (x:ref int) : unit = x := f a
why3 answers:
why3 prove ghost.mlw
File "ghost.mlw", line 5, characters 37-38:
warning: Logical symbol a is used in a non-ghost context
File "ghost.mlw", line 5, characters 32-34:
This expression makes a ghost modification in the non-ghost variable x
I'm surprised that the first message is a warning and not an error.
To tell all, it was in a much larger context where it appeared to be quite hard to figure out the reason of the dreadful message This expression makes a ghost modification in the non-ghost variable
at the beginning I thought that f
was assumed ghost, turning the first message into an error would have been helpful