tests/loop7.scop

   1 start: 40
   2 end: 114
   3 indent: "\t"
   4 context: '{  :  }'
   5 schedule: '{ domain: "{ S_3[t] : t >= 0; S_0[]; S_5[]; S_2[t] : t >= 0; S_6[]; S_4[t]
   6   : t >= 0; S_1[] }", child: { sequence: [ { filter: "{ S_0[] }" }, { filter: "{ S_1[]
   7   }" }, { filter: "{ S_3[t]; S_2[t]; S_4[t] }", child: { schedule: "L_0[{ S_4[t] ->
   8   [(t)]; S_2[t] -> [(t)]; S_3[t] -> [(t)] }]", child: { sequence: [ { filter: "{ S_2[t]
   9   }" }, { filter: "{ S_3[t] }" }, { filter: "{ S_4[t] }" } ] } } }, { filter: "{ S_5[];
  10   S_6[] }", child: { set: [ { filter: "{ S_5[] }" }, { filter: "{ S_6[] }" } ] } }
  11   ] } }'
  12 arrays:
  13 - context: '{  :  }'
  14   extent: '{ __pet_test_0[t] : t >= 0 }'
  15   value_bounds: '{ [i0] : 0 <= i0 <= 1 }'
  16   element_type: int
  17   element_size: 4
  18   uniquely_defined: 1
  19 - context: '{  :  }'
  20   extent: '{ a[] }'
  21   element_type: int
  22   element_size: 4
  23 - context: '{  :  }'
  24   extent: '{ i[] }'
  25   element_type: int
  26   element_size: 4
  27 statements:
  28 - line: 9
  29   domain: '{ S_0[] }'
  30   body:
  31     type: expression
  32     expr:
  33       type: op
  34       operation: =
  35       arguments:
  36       - type: access
  37         index: '{ S_0[] -> i[] }'
  38         reference: __pet_ref_0
  39         read: 0
  40         write: 1
  41       - type: call
  42         name: f
  43 - line: 10
  44   domain: '{ S_1[] }'
  45   body:
  46     type: expression
  47     expr:
  48       type: op
  49       operation: =
  50       arguments:
  51       - type: access
  52         index: '{ S_1[] -> i[] }'
  53         reference: __pet_ref_1
  54         read: 0
  55         write: 1
  56       - type: access
  57         index: '{ S_1[] -> i[] }'
  58         reference: __pet_ref_2
  59         read: 1
  60         write: 0
  61 - line: 10
  62   domain: '{ [S_2[t] -> [__pet_test_0 = 1]] : t >= 0 }'
  63   body:
  64     type: expression
  65     expr:
  66       type: op
  67       operation: =
  68       arguments:
  69       - type: access
  70         index: '{ S_2[t] -> __pet_test_0[(t)] }'
  71         reference: __pet_ref_4
  72         read: 0
  73         write: 1
  74       - type: op
  75         operation: <
  76         arguments:
  77         - type: access
  78           index: '{ S_2[t] -> i[] }'
  79           reference: __pet_ref_5
  80           read: 1
  81           write: 0
  82         - type: int
  83           value: 10
  84   arguments:
  85   - type: access
  86     index: '{ S_2[t] -> __pet_test_0[((-1 + t) : t > 0)] }'
  87     reference: __pet_ref_3
  88     read: 1
  89     write: 0
  90 - line: 11
  91   domain: '{ [S_3[t] -> [__pet_test_0 = 1]] : t >= 0 }'
  92   body:
  93     type: expression
  94     expr:
  95       type: op
  96       operation: =
  97       arguments:
  98       - type: access
  99         index: '{ S_3[t] -> a[] }'
 100         reference: __pet_ref_7
 101         read: 0
 102         write: 1
 103       - type: int
 104         value: 5
 105   arguments:
 106   - type: access
 107     index: '{ S_3[t] -> __pet_test_0[(t)] }'
 108     reference: __pet_ref_6
 109     read: 1
 110     write: 0
 111 - line: 10
 112   domain: '{ [S_4[t] -> [__pet_test_0 = 1]] : t >= 0 }'
 113   body:
 114     type: expression
 115     expr:
 116       type: op
 117       operation: +=
 118       arguments:
 119       - type: access
 120         index: '{ S_4[t] -> i[] }'
 121         reference: __pet_ref_9
 122         read: 0
 123         write: 1
 124       - type: int
 125         value: 1
 126   arguments:
 127   - type: access
 128     index: '{ S_4[t] -> __pet_test_0[(t)] }'
 129     reference: __pet_ref_8
 130     read: 1
 131     write: 0
 132 - line: -1
 133   domain: '{ S_5[] }'
 134   body:
 135     type: expression
 136     expr:
 137       type: op
 138       operation: kill
 139       arguments:
 140       - type: access
 141         killed: '{ S_5[] -> i[] }'
 142         index: '{ S_5[] -> i[] }'
 143         reference: __pet_ref_10
 144         kill: 1
 145 - line: -1
 146   domain: '{ S_6[] }'
 147   body:
 148     type: expression
 149     expr:
 150       type: op
 151       operation: kill
 152       arguments:
 153       - type: access
 154         killed: '{ S_6[] -> a[] }'
 155         index: '{ S_6[] -> a[] }'
 156         reference: __pet_ref_11
 157         kill: 1
 158 implications:
 159 - satisfied: 1
 160   extension: '{ __pet_test_0[t] -> __pet_test_0[t''] : 0 <= t'' <= t }'