--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on April 2012 ---
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