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
  • #804
Closed
Open
Issue created Nov 20, 2014 by Jochen Burghardt@burghardt

false assertion apparently undetected in the presence of overloaded virtual functions

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


Id Project Category View Due Date Updated
ID0001975 Frama-Clang Plug-in > clang public 2014-11-20 2015-02-23
Reporter Jochen Assigned To virgile Resolution open
Priority normal Severity minor Reproducibility always
Platform frama-c-Neon-20140301+dev-stance OS - OS Version xubuntu-cfe13.10
Product Version - Target Version - Fixed in Version -

Description :

Running "frama-c -wp -wp-rte" on the attached file generates 117 proof obligations of which 43 can be proven. I suppose that the obligation for the false assertion from line 19 is also proven, by qed; probably it has the name "typed_main_assert".

My reasons are:

If the assertion wasn't proven, an .mlw file for Alt-Ergo should appear in the wp-out directory which should contain the string "333"; however, no that string couldn't be found there, nor could "111"; while "222" occurs (in many/all .mlw files) only as value of the global variable "G__ZN6SquareE12_frama_c_vmt_221" which, in turn, is used only as index to an int array "t" and as an argument to "region" in global variables axioms, i.e. "222" doesn't occur in a goal.

If the value "333" in line 19 of file 139.cpp is changed to "222", i.e. if the assertion is made true, then the very same proof goal names and Valid/Unknown/Timeout results appear in the verification log. Similarly, if the value is changed to "111". All three log differ only in prover timings and obligation order, as can be seen by applying the shell-script "normalizeVerificationLog.sh" to the 117 obligation log lines in each of the log files "139_111orig.txt", "139_222orig.txt", and "139_333orig.txt" (all files attached).

Possibly, some precondition equivalent to \false is given to qed together with the goal for the line 19 assertion.

Attachments

  • 139.cpp
  • normalizeVerificationLog.sh
  • 139_111orig.txt
  • 139_222orig.txt
  • 139_333orig.txt
  • 139a.cpp
  • 139a.fc_log
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking