--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on May 2012 ---
On Mon, 2012-05-07 at 20:31 +0200, Claude Marche wrote: > /*@ requires \valid(AB_Ptr) && \valid(CD_Ptr); > @ behavior zero: > @ assumes \exact(*AB_Ptr) > \exact(*CD_Ptr) ; > @ ensures result == 1 > @ behavior one: > @ assumes \exact(*AB_Ptr) <= \exact(*CD_Ptr); > @ ensures result == 0; > @ */ I have a related question. Is \exact(x), when used in a precondition, equivalent to x (if x is a parameter of the function)? The example in the ACSL documention suggests it isn't. Are Coq or Gappa required to use \exact and is user interaction necessary to prove VCs? -- Best regards, Boris