Inline a function call during VC computation
Following several discussions and user requests, including that Zulip thread, this ticket is a feature wish to allow a user to declare that a given function, or a given function call, should be somehow inlined during VC computation. For example, in the code
val ref x : int
let incr () = x <- x+1
let test () = x <- 0; incr (); assert { x = 1 }
the assertion is not provable because of the lack of contract on incr
. It would be desirable to ask to inline the call to incr either by writing
let test () = x <- 0; [@vc:inline_call] incr (); assert { x = 1 }
or, to ask to inline all calls to incr
systematically
let incr [@vc:inline_calls] () = x <- x+1
Such an inlining should naturally be restricted to situationd where it is reasonable to do so, for example doing that on a recursive call would obviously be a bad idea.