--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on May 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie plugin



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