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

[Frama-c-discuss] Value Analysis and user-defined predicates



Dear list,

I am getting unexpected results with the value analysis plug-in, in
which basically boils down to the following code snippet:


/*@ predicate greater_than_zero(integer myval) = myval > 0; */
...
int a;
a =  10;
/*@ assert a > 0; */
/*@ assert greater_than_zero(a); */
...


I would expect the status "valid" for all "assert" above, but the
value analysis obstinately considers the second one as "unknown".

Could somebody by kind enough to point me at what I am doing wrong there?
Thanks in advance,
Sylvain