--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on April 2012 ---
Although, WP discharges the two, and more generally, the second one from the first ! L. Le 10 avr. 12 ? 15:04, sylvain nahas a ?crit : > 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 > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss