Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000259Frama-CPlug-in > value analysispublic2009-09-30 16:102014-02-12 16:55
Reporterdpariente 
Assigned Topascal 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090902 
Target VersionFixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000259: Problem with is_finite predicate generated by -val
DescriptionLaunching: 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
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000426)
virgile (developer)
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.

- Issue History
Date Modified Username Field Change
2009-09-30 16:10 dpariente New Issue
2009-09-30 16:10 dpariente Status new => assigned
2009-09-30 16:10 dpariente Assigned To => pascal
2009-09-30 16:50 virgile Note Added: 0000426
2009-09-30 16:50 virgile Status assigned => acknowledged
2009-10-19 17:59 svn Checkin
2010-12-02 23:13 svn Checkin
2010-12-02 23:13 svn Status acknowledged => resolved
2010-12-02 23:13 svn Resolution open => fixed
2010-12-10 15:45 signoles Fixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:37 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker