Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002299Frama-CPlug-in > wppublic2017-05-10 17:462017-05-10 17:46
Reporterboyer 
Assigned Tocorrenson 
PriorityhighSeverityblockReproducibilityalways
StatusassignedResolutionopen 
PlatformVirtualBox (Host Win7)OSUbuntuOS Version16.04.2
Product VersionFrama-C 14-Silicon 
Target VersionFixed in Version 
Summary0002299: Some ACSL mathematical functions crash WP
DescriptionSome 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.
Steps To ReproduceUsing 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
Additional InformationConsole 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.
[...]
TagsNo tags attached.
Attached Fileszip file icon wp-bug.zip [^] (817 bytes) 2017-05-10 17:46

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2017-05-10 17:46 boyer New Issue
2017-05-10 17:46 boyer Status new => assigned
2017-05-10 17:46 boyer Assigned To => correnson
2017-05-10 17:46 boyer File Added: wp-bug.zip


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker