Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / optim / wpdir / typed / toto_step_assert_23.ergo @ 6a93d814

History | View | Annotate | Download (1.22 KB)

1
(* ---------------------------------------------------------- *)
2
(* --- Assertion (file clocks7/clocks7_7.c, line 189)     --- *)
3
(* ---------------------------------------------------------- *)
4

    
5
goal toto_step_assert_23:
6
  forall i : int.
7
  forall t_6,t_5,t_4,t_3,t_2,t_1,t : (addr,int) farray.
8
  forall a : addr.
9
  let x = t_6[a] : int in
10
  let m = t_2[a <- 1] in
11
  P_trans_totoA ->
12
  is_sint32(i) ->
13
  is_sint32(t_1[a]) ->
14
  is_sint32(t_3[a]) ->
15
  is_sint32(t_4[a]) ->
16
  is_sint32(t_5[a]) ->
17
  is_sint32(x) ->
18
  (region(a.base) <= 0) ->
19
  (((i <= 0) ->
20
    ((t_6 = t[a <- 3]) and P_trans_totoB(i, 0) and
21
     (P_clock_b3(0) -> P_trans_b3(3)) and P_trans_totoH(i, 0, 3, 3) and
22
     (P_clock_d -> P_trans_d(i, 0)) and (P_clock_y -> P_trans_y(0, 3, 3, 3)))) and
23
   ((0 < i) ->
24
    ((t_5 = m) and (t_6 = m) and P_trans_totoB(i, 1) and
25
     P_trans_totoC(i, 1, 0) and P_trans_totoD(i, 1, 1) and
26
     P_trans_totoG(i, 1, 1) and (P_clock_b1(1, 1) -> P_trans_b1(1)) and
27
     (P_clock_c(1) -> P_trans_c(0, 1)) and (P_clock_d -> P_trans_d(i, 1)) and
28
     (P_clock_toto_2(1) -> P_trans_toto_2(i, 0)) and
29
     P_trans_totoF(i, 1, 1, 1, 1) and
30
     (P_clock_z(1) -> P_trans_z(1, 1, 1, 1)) and
31
     (P_clock_y -> P_trans_y(1, 1, 1, 1))))) ->
32
  P_trans_totoI(i, x)
33