--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on July 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Predicates fully supported in WP?



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