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](/uploads/9bb17093b31c46f1c71a4b8455b1c907/138.cpp) - [138.txt](/uploads/0d56b0f35ac408035605037a1316ad19/138.txt) - [_Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____10_Alt-Ergo.mlw](/uploads/8e72ed9402b727d86b81bb8cca28f534/_Z26_frama_c_find_dynamic_castP28_frama_c_rtti_name_info_____10_Alt-Ergo.mlw)