## 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).