--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on July 2012 ---
Hello, this code verifies with Jessie, but not with WP-0.5: //@ predicate f2{O, H}(int r, int x) = \at(r,H) == \at(x,H)+1; /*@ ensures f2{Old, Here}(\result, x); */ int f2(int x) { return x + 1; } Is the reason a lack of support of predicates in WP? -- Best regards, Boris