Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002232Frama-CPlug-in > wppublic2016-06-14 17:222016-06-14 17:22
Assigned Tocorrenson 
PlatformUnuntu 64-bitOSLinuxOS Version16.04
Product Version 
Target VersionFixed in Version 
Summary0002232: Use of very large real constants cause failures in proof generation in WP
DescriptionCode 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.
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/", line 159, characters 51-56
         Called from file "src/plugins/wp/", line 535, characters 8-22
         Called from file "src/libraries/stdlib/", line 334, characters 14-17
         Re-raised at file "src/libraries/stdlib/", line 334, characters 47-48
         Called from file "src/libraries/stdlib/", line 335, characters 2-12
         Called from file "src/libraries/stdlib/", line 335, characters 2-12
         Called from file "", line 134, characters 6-20
         Called from file "src/kernel_internals/runtime/", line 37, characters 4-20
         Called from file "src/kernel_services/cmdline_parameters/", line 787, characters 2-9
         Called from file "src/kernel_services/cmdline_parameters/", line 817, characters 18-64
         Called from file "src/kernel_services/cmdline_parameters/", line 228, characters 4-8

         Unexpected error (Invalid_argument("Unrecognized constant \"inf\"")).
         Please report as 'crash' at [^]
         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: [^]

== 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.
Additional InformationThis was tested in the public Aluminum version, on both a Linux and Cygwin build.
TagsNo tags attached.
Attached Filesc file icon bug.c [^] (49 bytes) 2016-06-14 17:22 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2016-06-14 17:22 jrobbins New Issue
2016-06-14 17:22 jrobbins Status new => assigned
2016-06-14 17:22 jrobbins Assigned To => correnson
2016-06-14 17:22 jrobbins File Added: bug.c

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker