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;

}

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.)