Skip to content
GitLab
Projects Groups Topics 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
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 171
    • Issues 171
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • 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
  • #371
Closed
Open
Issue created Feb 02, 2017 by Jochen Burghardt@burghardt

translation to why3 of int* argument to logic function

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


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

Description :

Running "frama-c -wp -wp-prover eprover foo.c" proves lemma "foo" in line 7, although it essentially says that no objects of type "int*" exist at all. The problem disappears if either (1) the result type "int" of "deref" is changed to "integer" in line 3, (2) "deref" is inlined at line 5, (3) "large" is inlined at line 7, or (4) "large(s) && !large(s)" is simplified to "\false" in line 7.

Using option "-wp-out", and comparing the files "Axiomatic.why" before and after change (1), see attached files "Axiomatic_int.why" and "Axiomatic_integer.why", reveals that the former has an "axiom Q_TL_deref" while the latter does not. This axiom essentially says that any value fetched from an integer array (i.e. a "map addr int" in why3 language) is already an int (i.e. satisfies "is_sint32" in why3 language), which imho is wrong.

When using "-wp alt-ergo" instead of "-wp eprover", the generated mlw files before and after change (1) literally agree, see attached file "lemma_foo_Alt-Ergo_int.mlw" and "lemma_foo_Alt-Ergo_integer.mlw"; they contain no occurrence of "deref" or "large".

The input given to eprover has been intercepted and boiled down as far as possible, resulting in file "foo_eprover_input.p" which is attached for convenience. Its axiom "q_TL_deref" in line 18 is a boiled-down translation of axiom "Q_TL_deref" from the why3 file, and is wrong as argued above.

Attachments

  • foo.c
  • Axiomatic_int.why
  • Axiomatic_integer.why
  • lemma_foo_Alt-Ergo_int.mlw
  • lemma_foo_Alt-Ergo_integer.mlw
  • foo_eprover_input.p
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking