--- layout: fc_discuss_archives title: Message 126 from Frama-C-discuss on October 2008 ---
Hi, Your problems come from the fact booleans terms and propositions are not the same, and provers do not treat them identically. * in the first one, I cannot prove the posts In this case, you attempt to treat everything as boolean terms, which is not the best thing to do with automatic provers. As a result, only Alt-Ergo manages to prove all the VC, while Simplify, Z3 and Yices fail on some. Maybe Jean-Christophe will have an idea why it is the case, maybe some problem with the encoding to SMT format? > > * in the second, the first post is proved, but the second post is > commented (syntax error) when you write @ //ensures \result == ((pcond3(pcond1(x),pcond2(y)))?1:0); you assume that pcond1, pcond2 and pcond3 are logic functions that return a boolean. This is not the case. In your example, these are predicates, whose application is a proposition that cannot be used inside terms. Please refer to the grammar of terms and propositions in ACSL reference (section 2.2), you will see a proposition cannnot occur as an argument of an application, and it can occur inside a proposition (a?b:c) only when b and c are themselves propositions. If you rewrite your example this way, all VC are proved by all the provers I mentioned: /*@ predicate pcond1(integer p) = (p>0)?\true:\false ; @ predicate pcond2(integer p) = (p<10)?\true:\false ; @*/ /*@ @ ensures (pcond1(x) && pcond2(y)) ==> \result == 1 ; @ ensures \result == 1 <==> pcond1(x) && pcond2(y); @*/ int ftest2(int x, int y) { return (x>0 && y<10); } Then, you may want to express this property with behaviors, in the following way: /*@ predicate pcond1(integer p) = p > 0; @ predicate pcond2(integer p) = p < 10; @*/ /*@ behavior ok: @ assumes pcond1(x) && pcond2(y); @ ensures \result == 1; @ behavior ko: @ assumes !pcond1(x) || !pcond2(y); @ ensures \result == 0; @*/ int ftest2(int x, int y) { return (x>0 && y<10); } HTH, -- Yannick -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081031/7aa7761e/attachment.html