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
  • #599
Closed
Open
Issue created Apr 30, 2015 by Jochen Burghardt@burghardt

invalid statement contract ("assigns") verified with CVC4 under strange circumstances

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


Id Project Category View Due Date Updated
ID0002110 Frama-Clang Plug-in > wp public 2015-04-30 2015-09-07
Reporter Jochen Assigned To correnson Resolution fixed
Priority normal Severity minor Reproducibility always
Platform Sodium-20150201 OS - OS Version xubuntu14.04
Product Version Frama-C Sodium Target Version - Fixed in Version -

Description :

Running "frama-c -wp-prover cvc4 -wp 473.c" on the attached file (referred to as version "(0)" in the modification discussion below) results in verifying all proof obligations, including the statement contract in line 27, which is obviously false, since "myRead" also assigns "fd->pos" (line 13) and definitely changes it (line 15). I can't see a contradiction from which line 27 could be proven.

CVC4 still proves all obligations if one of the following changes is made: (+1) myRead's "assigns" clauses in line 13 and 14 are joined into a single one, viz. "assigns fd->pos,*a;" (+2) all "requires" clauses in line 10-12 and 20-22 are commented-in simultaneously

CVC4 fails to prove the statement contract in line 27 if one of the following changes is made: (-1) myRead's "assigns" clauses in line 13 and 14 are swapped, (-2) myRead's "assigns" clauses in line 13 and 14 are joined into a single "assigns a,fd->pos;" (-3) the "ensures" clauses in line 15 is deleted (-4) the "ensures" clauses in line 23 (i.e. the whole contract) is deleted (-5) the type of "a" is changed from "struct A" to "int*" in line 17 and 25

From (+1) vs. (-2), as well as from (0) vs. (-1), it seems that the order of the memory location specifiers in myRead's "assigns" clause does matter. In (0) vs. (-4), the "ensures" clause of "myMain" apparently influences its body code.

Attachments

  • 473.c
  • wp-out.tar.gz
  • myMain_0b.why
  • myMain_0b1.smt2
  • myMain_0b2.smt2
  • myMain_0.smt2
  • myMain_-4.smt2
  • myMain_0.why
  • myMain_-4.why
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking