insufficient preconditions given to Alt-Ergo to prove "requires" clause about class member variable
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).