lustrec/optim/wpdir/typed/toto_step_assert_18.ergo @ 6a93d814
| 1 | 6a93d814 | xthirioux | (* ---------------------------------------------------------- *) |
|---|---|---|---|
| 2 | (* --- Assertion (file clocks7/clocks7_7.c, line 181) --- *) |
||
| 3 | (* ---------------------------------------------------------- *) |
||
| 4 | |||
| 5 | goal toto_step_assert_18: |
||
| 6 | forall i : int. |
||
| 7 | forall t_4,t_3,t_2,t_1,t : (addr,int) farray. |
||
| 8 | forall a : addr. |
||
| 9 | P_trans_totoA -> |
||
| 10 | P_clock_d -> |
||
| 11 | (i <= 0) -> |
||
| 12 | is_sint32(i) -> |
||
| 13 | is_sint32(t[a]) -> |
||
| 14 | is_sint32(t_1[a]) -> |
||
| 15 | is_sint32(t_2[a]) -> |
||
| 16 | is_sint32(t_3[a]) -> |
||
| 17 | is_sint32(t_4[a]) -> |
||
| 18 | (region(a.base) <= 0) -> |
||
| 19 | P_trans_d(i, 0) |