0002283: type of float parameter changed unexpectedly to double

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

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

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

Notes
(0006362) virgile (developer) 2017-02-24 19:59 edited on: 2017-03-01 18:18	The bug has been fixed in the development version, and the fix will appear in Phosphorus.

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