tests/for_while_init.scop

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