Frama-C Bug Tracking System - Frama-C
View Issue Details
0000259Frama-CPlug-in > Evapublic2009-09-30 16:102014-02-12 16:55
Frama-C Beryllium-20090902 
Frama-C Carbon-20101201-beta1 
0000259: Problem with is_finite predicate generated by -val
Launching: frama-c foo.c with foo.c (generated by "frama-c -val" on the original code) containing: /* Generated by Frama-C */ double f(double a , double b ) { double t ; t = 0.0; /*@ assert \is_finite("+", a, b); // synthesized assert \is_finite("*", a+b, a-b); // synthesized assert \is_finite("-", a, b); // synthesized */ t = (a + b) * (a - b); return (t); } yields: foo.c:13:[kernel] user error: syntax error while parsing annotation which seems to be due to multiple asserts in the same @-comment. Please note also that once the 3 asserts are 'exploded' into their own @-comment, then "frama-c foo.c" displays: foo.c:13:[kernel] user error: Error during annotations analysis: no such predicate or logic function \is_finite(char *, double , double ) (but this very last point was already discussed in other threads). Kernel seems to wait for a double typed expression parameter in \is_finite predicate, doesn't it? Like this single assert: //@ assert \is_finite((double)((a + b) * (a - b))); Regards, Dillon
No tags attached.
Issue History
2009-09-30 16:10dparienteNew Issue
2009-09-30 16:10dparienteStatusnew => assigned
2009-09-30 16:10dparienteAssigned To => pascal
2009-09-30 16:50virgileNote Added: 0000426
2009-09-30 16:50virgileStatusassigned => acknowledged
2009-10-19 17:59svnCheckin
2010-12-02 23:13svnCheckin
2010-12-02 23:13svnStatusacknowledged => resolved
2010-12-02 23:13svnResolutionopen => fixed
2010-12-10 15:45signolesFixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:37signolesStatusresolved => closed
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva

2009-09-30 16:50   
There are indeed two bugs in one - The pretty-printer should output typable code (i.e. one assert per annotation). - The assertions generated by value analysis regarding floats are still very exeperimental, and in particular there's no guarantee that they make sense with respect to ACSL standard library.