| 1 |
6a93d814
|
xthirioux
|
(* ---------------------------------------------------------- *)
|
| 2 |
|
|
(* --- Assertion (file clocks7/clocks7_7.c, line 176) --- *)
|
| 3 |
|
|
(* ---------------------------------------------------------- *)
|
| 4 |
|
|
|
| 5 |
|
|
goal toto_step_assert_16:
|
| 6 |
|
|
forall i : int.
|
| 7 |
|
|
forall t_3,t_2,t_1,t : (addr,int) farray.
|
| 8 |
|
|
forall a : addr.
|
| 9 |
|
|
P_trans_totoA ->
|
| 10 |
|
|
(0 < i) ->
|
| 11 |
|
|
is_sint32(i) ->
|
| 12 |
|
|
is_sint32(t[a]) ->
|
| 13 |
|
|
is_sint32(t_1[a]) ->
|
| 14 |
|
|
is_sint32(t_2[a]) ->
|
| 15 |
|
|
is_sint32(t_3[a]) ->
|
| 16 |
|
|
P_trans_totoB(i, 1) ->
|
| 17 |
|
|
P_trans_totoC(i, 1, 0) ->
|
| 18 |
|
|
P_trans_totoD(i, 1, 1) ->
|
| 19 |
|
|
(P_clock_b1(1, 1) -> P_trans_b1(1)) ->
|
| 20 |
|
|
(P_clock_c(1) -> P_trans_c(0, 1)) ->
|
| 21 |
|
|
(region(a.base) <= 0) ->
|
| 22 |
|
|
(P_clock_d -> P_trans_d(i, 1)) ->
|
| 23 |
|
|
(P_clock_toto_2(1) -> P_trans_toto_2(i, 0)) ->
|
| 24 |
|
|
P_trans_totoF(i, 1, 1, 1, 1) ->
|
| 25 |
|
|
(P_clock_z(1) -> P_trans_z(1, 1, 1, 1)) ->
|
| 26 |
|
|
P_trans_totoG(i, 1, 1)
|