Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • 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 208
    • Issues 208
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #367

Closed
Open
Created Feb 27, 2017 by Jochen Burghardt@burghardt

lemma tacitly omitted from prover assumptions

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


Id Project Category View Due Date Updated
ID0002286 Frama-C Plug-in > wp public 2017-02-27 2017-02-27
Reporter Jochen Assigned To correnson Resolution open
Priority normal Severity minor Reproducibility always
Platform Silicon-20161101 OS xubuntu OS Version -
Product Version Frama-C 14-Silicon Target Version - Fixed in Version -

Description :

Running "frama-c -wp -wp-rte -wp-prop=addIncAdd -wp-prover z3 bug1.c" on the attached file verifies the given goal "addIncAdd" in 40ms. However, when the closing brace is moved from line 35 up to line 30, no proof is found in 10s.

A "diff -r" on the wp-out directories shows that the translation of lemma "incAdd" is put into file "A_addAxioms.why" in the former, but into "Axiomatic2.why" in the latter case.

Intercepting the input if "z3" shows that only in the former case the translation is included in the input of "z3"; in the latter case it is missing.

I couldn't find the reason for just omitting "incAdd": exchanging lemmas "incAdd" and "addAdd" in the C source and comparing the "z3" inputs again shows that still "incAdd" is omitted; so the reason could be in it's name of form, but not in it place in source.

Attachments

  • bug1.c
  • why_495d09_Axiomatic2-T-Q_addIncAdd.smt2
  • why_767c25_Axiomatic2-T-Q_addIncAdd.smt2
  • why_54d12d_Axiomatic2-T-Q_addIncAdd.smt2
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking