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