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

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



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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120302/b7cac0e5/attachment.htm>