--- layout: fc_discuss_archives title: Message 18 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



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