ID0002232: **This issue was created automatically from Mantis Issue 2232. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002232 | Frama-C | Plug-in > wp | public | 2016-06-14 | 2016-06-14 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | jrobbins | **Assigned To** | correnson | **Resolution** | open | | **Priority** | normal | **Severity** | crash | **Reproducibility** | always | | **Platform** | Ununtu 64-bit | **OS** | Linux | **OS Version** | 16.04 | | **Product Version** | - | **Target Version** | - | **Fixed in Version** | - | ### Description : Code that uses real constants larger than the size of a double cause a failure to prove, even with true assertions. When WP tries to create the proof for files containing those constants, the kernel crashes with the message of Invalid_argument("Unrecognized constant \"inf\"") in the middle of generating the files to send to the prover. ### Additional Information : This was tested in the public Aluminum version, on both a Linux and Cygwin build. ### Steps To Reproduce : == File bug.c (attached): int main() { //@ assert 1.0 < 0x1.0p2047; } == Run command: frama-c bug.c -wp -wp-print == Output: [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing bug.c (with preprocessing) [wp] warning: Missing RTE guards [wp] 1 goal scheduled [wp] [Alt-Ergo] Goal typed_main_assert : Failed Invalid_argument("Unrecognized constant \"inf\"") [wp] Proved goals: 0 / 1 Alt-Ergo: 0 (failed: 1) ------------------------------------------------------------ Function main ------------------------------------------------------------ Goal Assertion (file bug.c, line 2): Prove: .1e0 < [kernel] Current source was: bug.c:1 The full backtrace is: Raised at file "src/kernel_services/plugin_entry_points/log.ml", line 159, characters 51-56 Called from file "src/plugins/wp/register.ml", line 535, characters 8-22 Called from file "src/libraries/stdlib/extlib.ml", line 334, characters 14-17 Re-raised at file "src/libraries/stdlib/extlib.ml", line 334, characters 47-48 Called from file "src/libraries/stdlib/extlib.ml", line 335, characters 2-12 Called from file "src/libraries/stdlib/extlib.ml", line 335, characters 2-12 Called from file "queue.ml", line 134, characters 6-20 Called from file "src/kernel_internals/runtime/boot.ml", line 37, characters 4-20 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 787, characters 2-9 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 817, characters 18-64 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8 Unexpected error (Invalid_argument("Unrecognized constant \"inf\"")). Please report as 'crash' at http://bts.frama-c.com/. Your Frama-C version is Aluminium-20160501. Note that a version and a backtrace alone often do not contain enough information to understand the bug. Guidelines for reporting bugs are at: http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines == Note that the constant "0x1.0p2047" can be replaced with any value greater than or equal to 0x2.0p1023; even other forms of real constant other than hexadecimal. ## Attachments - [bug.c](/uploads/8354bd56c66b755df3ee5650534570dd/bug.c)