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 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • 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
  • #2343

Closed
Open
Created Oct 22, 2010 by Jochen Burghardt@burghardt

separately verified files show code-bug when linked together

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


Id Project Category View Due Date Updated
ID0000615 Frama-C Plug-in > jessie public 2010-10-22 2010-10-22
Reporter Jochen Assigned To cmarche Resolution open
Priority normal Severity major Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Boron-20100401 Target Version - Fixed in Version -

Description :

The attached file contains the files "ftest3a.c" and "ftestMain.c. Each of them can be verified (by alt-ergo), except for "\valid(&b)" in ftestMain, cf. issue #614. Although the "assert res == 1" in ftestMain is verified, it does not hold, as can be seen by removing both "////"-comments, compiling, and running: "gcc ftest3a.c ftestMain.c && ./a.out" yields "main: res=0\n" on stdout. Note that the contracts of "f()" and "g()" are identical across both files, and that they don't omit neccessary or provide invalid preconditions (e.g. no "assigns \nothing"). Also, the "no-regions"-model is used in both files. The parameter "x" in "g()" is an alias to the global "b", and "f()" modifies "b". Both facts can be detected only by looking into ftestMain. Hence, by looking into ftest3a only, it cannot be detected that "g"s ensures clause is wrong; there is no other hint than nonexistent "assigns"-clauses.

Attachments

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