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.
|ID0001974||Frama-Clang||Plug-in > clang||public||2014-11-17||2015-02-16|
|Product Version||-||Target Version||-||Fixed in Version||-|
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.