--- layout: fc_discuss_archives title: Message 125 from Frama-C-discuss on October 2008 ---
Hello, I encounter some difficulties with predicates and logic functions. Here is two very small exemples. The first one is made with logic functions whereas the other one is made with predicates. * in the first one, I cannot prove the posts * in the second, the first post is proved, but the second post is commented (syntax error) Can you see my problems ? thanks in advance, St?phane /*@ logic boolean cond1(integer p) = (p>0)?\true:\false ; @ logic boolean cond2(integer p) = (p<10)?\true:\false ; @ logic boolean cond3(boolean c1, boolean c2) = c1 && c2 ; @*/ /*@ @ ensures (cond1(x) && cond2(y)) ==> \result == 1 ; @ ensures \result == ((cond3(cond1(x),cond2(y)))?1:0); @*/ int ftest(int x, int y) { return (x>0 && y<10); } /*@ predicate pcond1(integer p) = (p>0)?\true:\false ; @ predicate pcond2(integer p) = (p<10)?\true:\false ; @ predicate pcond3(boolean c1, boolean c2) = c1 && c2 ; @*/ /*@ @ ensures (pcond1(x) && pcond2(y)) ==> \result == 1 ; @ //ensures \result == ((pcond3(pcond1(x),pcond2(y)))?1:0); @*/ int ftest2(int x, int y) { return (x>0 && y<10); }