2021-03-01 04:23 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002283Frama-CPlug-in > wppublic2017-02-24 12:112017-05-31 19:05
Reporterwidc 
Assigned Tocorrenson 
PriorityhighSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSUbuntuOS Version16.04 LTS
Product VersionFrama-C 14-Silicon 
Target VersionFixed in VersionFrama-C 15-Phosphorus 
Summary0002283: type of float parameter changed unexpectedly to double
DescriptionCurrent 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 ReproduceC 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 InformationQuick solution would be appreciated.
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0006362

virgile (developer)

2017-02-24 19:59

Last edited: 2017-03-01 18:18

View 3 revisions

 The bug has been fixed in the development version, and the fix will appear in Phosphorus.
+Notes

-Issue History
Date Modified Username Field Change
2017-02-24 12:11 widc New Issue
2017-02-24 12:11 widc Status new => assigned
2017-02-24 12:11 widc Assigned To => correnson
2017-02-24 19:59 virgile Note Added: 0006362
2017-02-24 19:59 virgile Status assigned => resolved
2017-02-24 19:59 virgile Fixed in Version => Frama-C GIT, precise the release id
2017-02-24 19:59 virgile Resolution open => fixed
2017-03-01 10:28 yakobowski Note Edited: 0006362 View Revisions
2017-03-01 18:18 virgile Note Edited: 0006362 View Revisions
2017-05-31 19:04 signoles Fixed in Version Frama-C GIT, precise the release id =>
2017-05-31 19:04 signoles Fixed in Version => Frama-C 15-Phosphorus
2017-05-31 19:05 signoles Status resolved => closed
+Issue History