--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on March 2012 ---
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>