"unlisted write effect" : misleading error message
On the following code, which is a reduced version of a much larger example
val ref z :int
val g () : unit
writes { z }
ensures { z = z }
let f ()
writes { }
ensures { z = z }
=
let ref y = 42 in
y <- 2;
(* a lot of lines of code *)
g()
Why3 emits the message this expression produces an unlisted write effect
located on expression y <- 2
. This is badly located, since it is the expression g()
that produces the unlisted write effect on z
. It is particularly misleading as it tends to pretend that the unlisted write effect is on y
, which is wrong since y
is local.
It would be nice to:
- Fix the localization of the message, so as it points to
g()
- Make the error message more precise, by explicitating the offending write effects in question, e.g.
this expression produces an unlisted write effect on z