Skip to content

GitLab

  • Menu
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 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
  • #870

Closed
Open
Created Nov 17, 2014 by Jochen Burghardt@burghardt

insufficient preconditions given to Alt-Ergo to prove obligation originating from virtual methods

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


Id Project Category View Due Date Updated
ID0001974 Frama-Clang Plug-in > clang public 2014-11-17 2015-02-16
Reporter Jochen Assigned To virgile Resolution duplicate
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 138.cpp" on the attached 9-line program generates 98 proof obligations of which 71 turn out to be unprovable (by Qed and Alt-Ergo) after a total user-time of 3 minutes (see session protocol in file "138".txt"). These figures by their own may indicate a problem in scaling-up the current approach to C++ inheritance and virtual functions.

A closer look at e.g. the file "_Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____10_Alt-Ergo.mlw" shows that Alt-Ergo is given insufficient preconditions to prove the goal

"forall i_2,i_1,i : int. forall t_2,t_1 : (addr,int) farray. ... -> is_sint32(i_2) -> is_sint32(t_2[...]) -> -2147483648 <= i_2 + t_2[...]".

Neither "i_2" nor "t_2" appear in the goal formula, except in the shown slice. Knowing that both i_2 and t_2[...] are signed 32-bit ints is insufficient to prove that their sum won't underflow.

Attachments

  • 138.cpp
  • 138.txt
  • _Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____10_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