Problem with is_finite predicate generated by -val
ID0000259: This issue was created automatically from Mantis Issue 259. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000259 | Frama-C | Plug-in > Eva | public | 2009-09-30 | 2014-02-12 |
| Reporter | dpariente | Assigned To | pascal | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Beryllium-20090902 | Target Version | - | Fixed in Version | Frama-C Carbon-20101201-beta1 |
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