ID0002014: **This issue was created automatically from Mantis Issue 2014. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002014 | Frama-Clang | Plug-in > clang | public | 2014-12-04 | 2015-02-18 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **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 : In the attached program "188.cpp", the constructor "X()" initialized the class member variable "x" to 13 (contract and code in line 4 and 5, respectively; contract deliberately phrased to prevent Qed from using it). This constructor is called from the declaration in line 12. The "assert" in line 13 can be proved without problems; however, the (literally identical) precondition of the "foo" call in line 14 cannot. The file "main_assert_Alt-Ergo.mlw" for the "assert" has the goal: 823 goal main_assert: 824 let a = shiftfield_F__Z1X_x(shift__Z1X(global(L_i_105), 0)) : addr in 825 forall t : int farray. 826 forall t_1 : (addr,int) farray. 827 linked(t) -> 828 (130 = (10 * t_1[a])) -> 829 is_sint32(t_1[a]) -> 830 (t_1[a] <= 42) that is, t_1[a]==13 is known and t_1[a]<=42 is to be proved. In contrast, the file "main_call__Z3foo1X_pre_Alt-Ergo.mlw" for the "requires" has the goal: 824 goal main_call__Z3foo1X_pre: 825 let a = shiftfield_F__Z1X_x(shift__Z1X(global(L_i_105), 0)) : addr in 826 let a_1 = shift__Z1X(global(L___fc_tmp_0_106), 0) : addr in 827 forall t : int farray. 828 forall t_2,t_1 : (addr,int) farray. 829 linked(t) -> 830 (t_1[a] <= 42) -> 831 (130 = (10 * t_1[a])) -> 832 IsS__Z1X(Load_S__Z1X(a_1, t_2)) -> 833 is_sint32(t_1[a]) -> 834 ((Load_S__Z1X(a_1, t_2).F__Z1X_x) <= 42) that is, t_1[a]==13 is known and (Load_S__Z1X(a_1, t_2).F__Z1X_x)<=42 is to be proven, where no relation between t_1 and t_2 is known (both are locally quantified variables). I guess both proof goals should be similar, or at least a relation between t_1 and t_2 should be given to Alt-Ergo in the goal stemming from "requires". If "assigns x;" is added to the contract of "X()" in line 4, the situation doesn't improve. The goals then look as follows. In file "main_assert_Alt-Ergo.mlw": 759 goal main_assert: 760 forall i : int. 761 forall t : int farray. 762 (130 = (10 * i)) -> 763 linked(t) -> 764 is_sint32(i) -> 765 (i <= 42) that is, i==13 is known and i<=42 is to be proved. In file "main_call__Z3foo1X_pre_Alt-Ergo.mlw": 824 goal main_call__Z3foo1X_pre: 825 let a = shift__Z1X(global(L___fc_tmp_0_106), 0) : addr in 826 forall i : int. 827 forall t : int farray. 828 forall t_1 : (addr,int) farray. 829 (i <= 42) -> 830 (130 = (10 * i)) -> 831 linked(t) -> 832 is_sint32(i) -> 833 IsS__Z1X(Load_S__Z1X(a, t_1)) -> 834 ((Load_S__Z1X(a, t_1).F__Z1X_x) <= 42) that is, i==13 is known and (Load_S__Z1X(a, t_1).F__Z1X_x)<=42 is to be proven, where no relation between i and t_1 is known (again, both are locally quantified variables). ## Attachments - [188.cpp](/uploads/099b24b3b63f23a0b2d36961399b08f8/188.cpp) - [main_assert_Alt-Ergo.mlw_without_assigns](/uploads/a178b5c1643ad780e1b69564d3ddd595/main_assert_Alt-Ergo.mlw_without_assigns) - [main_call__Z3foo1X_pre_Alt-Ergo.mlw_without_assigns](/uploads/9353ccdc4d04963494c985a23d4a60a5/main_call__Z3foo1X_pre_Alt-Ergo.mlw_without_assigns) - [main_assert_Alt-Ergo.mlw_with_assigns](/uploads/1763b58af26b99be4ae48ee3bbc91da3/main_assert_Alt-Ergo.mlw_with_assigns) - [main_call__Z3foo1X_pre_Alt-Ergo.mlw_with_assigns](/uploads/926b2e468083e8df93a34ec6b80db691/main_call__Z3foo1X_pre_Alt-Ergo.mlw_with_assigns)