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);

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)));

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.