|
1
|
(* ---------------------------------------------------------- *)
|
|
2
|
(* --- Assertion (file clocks7/clocks7_7.c, line 169) --- *)
|
|
3
|
(* ---------------------------------------------------------- *)
|
|
4
|
|
|
5
|
goal toto_step_assert_12:
|
|
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
|
(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
|
is_sint32(t_4[a]) ->
|
|
17
|
P_trans_totoB(i, 1) ->
|
|
18
|
P_trans_totoC(i, 1, 0) ->
|
|
19
|
(P_clock_c(1) -> P_trans_c(0, 1)) ->
|
|
20
|
(region(a.base) <= 0) ->
|
|
21
|
(P_clock_d -> P_trans_d(i, 1)) ->
|
|
22
|
(P_clock_toto_2(1) -> P_trans_toto_2(i, 0)) ->
|
|
23
|
P_trans_totoD(i, 1, 1)
|
|
24
|
|