Frama-C Bug Tracking System - Frama-C
View Issue Details
0002299Frama-CPlug-in > wppublic2017-05-10 17:462017-05-10 17:46
boyer 
correnson 
highblockalways
assignedopen 
VirtualBox (Host Win7)Ubuntu16.04.2
Frama-C 14-Silicon 
 
0002299: Some ACSL mathematical functions crash WP
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.
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
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.
[...]
No tags attached.
zip wp-bug.zip (817) 2017-05-10 17:46
https://bts.frama-c.com/file_download.php?file_id=1174&type=bug
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: wp-bug.zip

There are no notes attached to this issue.