Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Using a identifier in an "assumes" clause

  • Subject: [Frama-c-discuss] Using a identifier in an "assumes" clause
  • From: Patrick.Baudin at cea.fr (BAUDIN Patrick)
  • Date: Mon, 05 Mar 2012 08:53:49 +0100
  • In-reply-to: <CAEm-Qw0viAaMQpDcxnjTAT_hfe=do8KHBPGi9kJgweccLMzPoA@mail.gmail.com>
  • References: <CAEm-Qw0viAaMQpDcxnjTAT_hfe=do8KHBPGi9kJgweccLMzPoA@mail.gmail.com>
Hello,

Your problem comes from a lack of alt-ergo.
As you can see in this example, the goal ok and ko are equivalent.
Alt-ergo 0.94 can only prove the first one :
 > cat test.why
goal ko:
   forall b_0:int. forall a_0:int.
   (let diff_0 = (a_0-b_0) in (0 <= diff_0))
   -> ((a_0 < b_0) -> (b_0 = a_0))
goal ko:
   forall b_0:int. forall a_0:int.
   (forall diff_0:int. (diff_0 = (a_0-b_0)) -> (0 <= diff_0))
   -> ((a_0 < b_0) -> (b_0 = a_0))
 >alt-ergo test.why
Inconsistent assumption
File "test.why", line 1, characters 1-150:File "test.why", line 1, 
characters 1-150:Valid (0.0100) (2)
File "test.why", line 5, characters 1-176:I don't know

Now, WP plugin translates \let constructs of ACSL into forall and 
equalities constructs of Alt-ergo in order to work around a bug of 
alt-ergo 0.93.
The option "-wp-norm Let" can be used to keep let constructs into goals 
for alt-ergo.
With this option, your two goals can be verified.

When subtitution does not give too big goals, you can also use the 
option  "-wp-norm Exp"

 > frama-c -wp-help
...
-wp-norm <norm>     Predicate normalization for Coq and Alt-Ergo provers:
                     - Eqs: replace let-bindings by equalities (default).
                     - Let: preserve let-bindings.
                     - Exp: let-expansion.
                     - Cc:  generates local functions by closure-conversion
...

Patrick.



02/03/2012 17:30, mohamed belasri wrote:
> Hi,
>
> I tried to verify the following example by using an identifier (diff) to
> simplify the assumption :
> /*@
>    @ behavior b1:
>    @     assumes      \let diff=(a-b);         diff>=0;
>    @     ensures \result==a;
>    @ behavior b2:
>    @     assumes      \let diff=(a-b);        diff<0;
>    @     ensures \result==b;
>    @ complete behaviors;
>    @ disjoint behaviors;
>    @*/
>
> int max(int a, int b){
>      if(a>=b)
>          return a;
>      else
>          return b;
> }
>
> but I realized that the WP plug-in couldn't verify that the assumption
> "diff>=0" is equivalent to "a>=b", so he could not verify for example that
> \result==a.
> However, we can easily verify the same function if don't use an identifier :
> /*@
>    @ behavior b1:
>    @     assumes     (a-b)>=0;
>    @     ensures \result==a;
>    @ behavior b2:
>    @     assumes    (a-b)<0;
>    @     ensures \result==b;
>    @ complete behaviors;
>    @ disjoint behaviors;
>    @*/
>
> So, if anyone know why we have such a problem ...
>
> Regards.
>