Add warning to anonymous function without ensures
In the following program, the contract of the intermediate function is not inferred automatically by Why3 (it apparently cannot be in the general case): in particular, the assignment to b is not reflected in the generated tasks. This issue is for generating a warning when such function do not carry a postcondition:
use int.Int
use int.MinMax
use ref.Ref
let f3 (a b : ref int) (c d: int)
requires { c < d }
ensures { result = min c d /\ !b = 22 }
=
a :=
(fun () -> if c < d then
(b := 4; c)
else
d) (* Here we should probably add a postcondition *) ();
!a + !b