Project

General

Profile

Download (443 Bytes) Statistics
| Branch: | Tag: | Revision:
1
(* ---------------------------------------------------------- *)
2
(* --- Assertion (file clocks7/clocks7_7.c, line 149)     --- *)
3
(* ---------------------------------------------------------- *)
4

    
5
goal toto_step_assert:
6
  forall t_4,t_3,t_2,t_1,t : (addr,int) farray.
7
  forall a : addr.
8
  is_sint32(t[a]) ->
9
  is_sint32(t_1[a]) ->
10
  is_sint32(t_2[a]) ->
11
  is_sint32(t_3[a]) ->
12
  is_sint32(t_4[a]) ->
13
  (region(a.base) <= 0) ->
14
  P_trans_totoA
15

    
(2-2/55)