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.