lustrec/optim/wpdir/typed/toto_step_assert_18.ergo @ 6a93d814
| 1 |
(* ---------------------------------------------------------- *) |
|---|---|
| 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) |
| 20 |
|