Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 201
    • Issues 201
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #507
Closed
Open
Created Jun 14, 2016 by mantis-gitlab-migration@mantis-gitlab-migration

Use of very large real constants cause failures in proof generation in WP

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
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking