Skip to content
GitLab
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 173
    • Issues 173
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and 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
  • #1192
Closed
Open
Issue created Dec 16, 2013 by Loïc Correnson@lcorrensonDeveloper

Bug in let-elimination (due to <==> and assert false).

ID0001586: This issue was created automatically from Mantis Issue 1586. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0001586 Frama-C Plug-in > wp public 2013-12-16 2014-03-13
Reporter correnson Assigned To correnson Resolution fixed
Priority normal Severity major Reproducibility have not tried
Platform - OS - OS Version -
Product Version - Target Version - Fixed in Version Frama-C Neon-20140301

Description :

Bug in let-elimination (due to <==> and assert false). Using -wp-no-let makes the assert false not-proved as expected.

Additional Information :

In the attached program, we have no assumption and everything is proved with WP (Frama-C Fluorine June), including the assert 1==2 in case N!

frama-c-gui -pp-annot -wp -wp-rte q19_switch_fun_call.c

It appears that the issue is coming from the equivalences used in the behaviours of compute_trans(). If we replace "<==>" by "==>", then the 1==2 assert is not proved (substitute call to compute_trans() by compute_trans2() in main()).

In both cases (compute_trans() and compute_trans2()), the contract is always proved.

Attachments

  • q19_switch_fun_call.c
  • q20_switch_fun_call.c
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking