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