| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] |
| ID | Project | Category | View Status | Date Submitted | Last Update |
| 0002283 | Frama-C | Plug-in > wp | public | 2017-02-24 12:11 | 2017-05-31 19:05 |
|
| Reporter | widc | |
| Assigned To | correnson | |
| Priority | high | Severity | minor | Reproducibility | always |
| Status | closed | Resolution | fixed | |
| Platform | | OS | Ubuntu | OS Version | 16.04 LTS |
| Product Version | Frama-C 14-Silicon | |
| Target Version | | Fixed in Version | Frama-C 15-Phosphorus | |
|
| Summary | 0002283: type of float parameter changed unexpectedly to double |
| 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) {
... |
| 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;
}
1. Run:
frama-c-gui sgn.c
2. Select the post-condition
3. 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.) |
| Additional Information | Quick solution would be appreciated. |
| Tags | No tags attached. |
|
| Attached Files | |
|
Relationships 
Relationships