| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0000259 | Frama-C | Plug-in > Eva | public | 2009-09-30 16:10 | 2014-02-12 16:55 | ||||
| Reporter | dpariente | ||||||||
| Assigned To | pascal | ||||||||
| Priority | normal | Severity | minor | Reproducibility | always | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C Beryllium-20090902 | ||||||||
| Target Version | Fixed in Version | Frama-C Carbon-20101201-beta1 | |||||||
| Summary | 0000259: Problem with is_finite predicate generated by -val | ||||||||
| Description | 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 | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
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. |
| Notes |
| 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 | ||
| 2010-12-02 23:13 | svn | ||
| 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 |
| 2013-12-19 01:12 | pascal | Source_changeset_attached | => framac master 6f2fafed |
| 2013-12-19 01:13 | Source_changeset_attached | => framac master db507548 | |
| 2014-02-12 16:55 | pascal | Source_changeset_attached | => framac stable/neon 6f2fafed |
| 2014-02-12 16:55 | Source_changeset_attached | => framac stable/neon db507548 | |
| 2018-01-12 14:26 | signoles | Category | Plug-in > value analysis => Plug-in > Eva |
| Issue History |