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 174
    • Issues 174
    • 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
  • #2380
Closed
Open
Issue created Feb 25, 2010 by Jochen Burghardt@burghardt

same formula translated differently as axiom/lemma

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


Id Project Category View Due Date Updated
ID0000420 Frama-C Plug-in > jessie public 2010-02-25 2010-04-19
Reporter Jochen Assigned To cmarche Resolution fixed
Priority normal Severity minor Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Beryllium-20090902 Target Version - Fixed in Version Frama-C Boron-20100401

Description :

Axiom ax2 (line 5,6 in attached file) is translated into a proof obligation on 2 memory labels. However, in lemma lm1 (line 11,12), the literally same formula is translated into a proof obligation on 4 memory labels; and so is the assertion in line 24, which is an instance of the ax2/lm1 formula.

As a consequence, when lm1 is omitted, the assertion cannot be proved (by Alt-ergo; Simplify doesnt prove it in any case); but when lm1 is present, the assertion can be proved, while the lemma itself can not.

(While the example program in the attached file is nonsensical, it has been boiled down from a program that does make sense.)

Attachments

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