Some ACSL mathematical functions crash WP
ID0002299: This issue was created automatically from Mantis Issue 2299. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002299 | Frama-C | Plug-in > wp | public | 2017-05-10 | 2017-05-10 |
| Reporter | boyer | Assigned To | correnson | Resolution | open |
| Priority | high | Severity | block | Reproducibility | always |
| Platform | VirtualBox (Host Win7) | OS | Ubuntu | OS Version | 16.04.2 |
| Product Version | Frama-C 14-Silicon | Target Version | - | Fixed in Version | - |
Description :
Some of the mathematical functions enumerated in http://frama-c.com/download/acsl.pdf, p24 are not correctly supported by Frama-c. For instance, the keywords \pow, \cos and \sin are recognized at parsing and supported by EVA whereas an error is reported for WP (builtin functions are not defined) followed by an internal error.
Additional Information :
Console message:
[kernel] Parsing .opam/4.04.0/share/frama-c/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing ex.c (with preprocessing) [wp] Running WP plugin... [wp] warning: Missing RTE guards [wp] user error: Builtin \round_error(float32) not defined [wp] failure: Logic '\round_error' undefined
Crash report:
Current source was: :0 The full backtrace is: Raised at file "hashtbl.ml", line 440, characters 17-32 Called from file "src/libraries/project/state_topological.ml", line 62, characters 23-38
Plug-in wp aborted: internal error. Reverting to previous state. [...]
Steps To Reproduce :
Using Example 2.9, p25 from the ACSL manual: /@ requires \abs(\exact(x)) <= 0x1p-5; @ requires \round_error(x) <= 0x1p-20; @ ensures \abs(\exact(\result)-\cos(\exact(x))) <= 0x1p-24; @ ensures \round_error(\result) <= \round_error(x) + 0x3p-24; @/ float cosine(float x) { return 1.0f - x * x * 0.5f; } Then: frama-c-gui -wp cosine.c