Frama-C Bug Tracking System - Frama-C
View Issue Details
0002299Frama-CPlug-in > wppublic2017-05-10 17:462017-05-10 17:46
VirtualBox (Host Win7)Ubuntu16.04.2
Frama-C 14-Silicon 
0002299: Some ACSL mathematical functions crash WP
Some of the mathematical functions enumerated in, [^] 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.
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;
frama-c-gui -wp cosine.c
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 "", line 440, characters 17-32
Called from file "src/libraries/project/", line 62, characters 23-38

Plug-in wp aborted: internal error.
Reverting to previous state.
No tags attached.
zip (817) 2017-05-10 17:46
Issue History
2017-05-10 17:46boyerNew Issue
2017-05-10 17:46boyerStatusnew => assigned
2017-05-10 17:46boyerAssigned To => correnson
2017-05-10 17:46boyerFile Added:

There are no notes attached to this issue.