type of float parameter changed unexpectedly to double
ID0002283: This issue was created automatically from Mantis Issue 2283. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002283 | Frama-C | Plug-in > wp | public | 2017-02-24 | 2017-05-31 |
| Reporter | widc | Assigned To | correnson | Resolution | fixed |
| Priority | high | Severity | minor | Reproducibility | always |
| Platform | - | OS | Ubuntu | OS Version | 16.04 LTS |
| Product Version | Frama-C 14-Silicon | Target Version | - | Fixed in Version | Frama-C 15-Phosphorus |
Description :
Current source was: sgn.c:4 The full backtrace is: Raised at file "hashtbl.ml", line 328, characters 23-32 Called from file "src/libraries/project/state_topological.ml", line 62, characters 23-38
Frama-C aborted: internal error. Your Frama-C version is Silicon-20161101.
From the floating_point.ml the following message is reported: Could not parse floating point number "-0x1.0000000000000p0"
The code in the main pane shows: float sgn(float u) ... if ((double)u > 0.0) { ...
Additional Information :
Quick solution would be appreciated.
Steps To Reproduce :
C code of sgn.c :
/*@
ensures A: \result == 1.0 || \result == 0.0 || \result == -1.0 ;
/
float sgn(float u)
{
float p; / return value */
if (u > 0.0) {
p = 1.0;
} else if (u < 0.0) {
p = -1.0;
} else {
p = 0.0;
}
return p;
}
- Run: frama-c-gui sgn.c
- Select the post-condition
- In context menu - Prove property by WP
(When the three "float" strings in the above code are changed to "double", the tool works fine, no error is reported.)