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
  • #106
Closed
Open
Issue created Oct 09, 2017 by Jochen Burghardt@burghardt

suggest unique term normalization for lemmas and goals

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


Id Project Category View Due Date Updated
ID0002329 Frama-C Plug-in > wp public 2017-10-09 2019-10-17
Reporter Jochen Assigned To correnson Resolution no change required
Priority normal Severity tweak Reproducibility always
Platform Phosphorus-20170501 OS - OS Version xubuntu 17.04
Product Version Frama-C 15-Phosphorus Target Version - Fixed in Version -

Description :

Running "frama-c -wp -wp-prop g aaa.c" on the attached file fails to prove the assertion "g", although it obviously follows from "f" by applying lemma "lem". One reason for that is of course the inherent incompleteness of SMT provers like Alt-Ergo and Cvc4. However, another reason is that Frama-C's term normalization(1) swaps some arguments of "+", and (2) performs swaps in the lemma that differ from those performed in the goal.

As a result, in the attached mlw file, "(L_Foo(a,b+c)=true) -> (L_Bar(a,c+d)=true)" appears in the lemma, while "(L_Foo(a,i_1+i_2)=true) -> (L_Bar(a,i+i_1)=true)" appears in the goal. The latter is equivalent to "(L_Foo(a,c+b)=true) -> (L_Bar(a,d+c)=true)" when expressed in a notation closer to the source-code. Variable "c" is common to L_Foo and L_Bar; note its different positions in the lemma vs. in the goal.

If the goal is changed to "(L_Foo(a,i_2+i_1)=true) -> (L_Bar(a,i_1+i)=true)", it syntactically matches the lemma, and Alt-Ergo proves it in a few milliseconds.

Unless there are good reasons to swap the arguments of "+", they should be kept in their source-code order; this way, the user has a chance to control what is given to the provers.

However, if there are good reasons to include argument swapping in term normalization, it should be performed in the same way both in lemmas and in goals.

A possible explanation for the above behavior of Frama-C is that, for some reason, source-code variable names are transformed to unrelated internal names in goals, but not in lemmas, and that term normalization just orders arguments of commutative functions lexicographically (cf. issue #2100 (closed)).

Attachments

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