tests/for_while_inc2.scop

   1 start: 83
   2 end: 234
   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         relation: '[n] -> { S1[x1] -> s[] }'
  33         index: '[n] -> { S1[x1] -> s[] }'
  34         reference: __pet_ref_0
  35         read: 0
  36         write: 1
  37       - type: call
  38         name: f
  39 - line: 13
  40   domain: '[n] -> { S_5[x1] : x1 <= -1 + n and x1 >= 0 }'
  41   schedule: '[n] -> { S_5[x1] -> [0, x1, 1, 0] }'
  42   body:
  43     type: expression
  44     expr:
  45       type: op
  46       operation: kill
  47       arguments:
  48       - type: access
  49         relation: '[n] -> { S_5[x1] -> x2[] }'
  50         index: '[n] -> { S_5[x1] -> x2[] }'
  51         reference: __pet_ref_1
  52         read: 0
  53         write: 0
  54 - line: 13
  55   domain: '[n] -> { S_1[x1] : x1 <= -1 + n and x1 >= 0 }'
  56   schedule: '[n] -> { S_1[x1] -> [0, x1, 1, 1] }'
  57   body:
  58     type: expression
  59     expr:
  60       type: op
  61       operation: =
  62       arguments:
  63       - type: access
  64         relation: '[n] -> { S_1[x1] -> x2[] }'
  65         index: '[n] -> { S_1[x1] -> x2[] }'
  66         reference: __pet_ref_2
  67         read: 0
  68         write: 1
  69       - type: int
  70         value: 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         relation: '[n] -> { S_2[x1, t] -> __pet_test_0[x1, t] }'
  82         index: '[n] -> { S_2[x1, t] -> __pet_test_0[(x1), (t)] }'
  83         reference: __pet_ref_4
  84         read: 0
  85         write: 1
  86       - type: call
  87         name: P
  88         arguments:
  89         - type: access
  90           relation: '[n] -> { S_2[x1, t] -> [x1] }'
  91           index: '[n] -> { S_2[x1, t] -> [(x1)] }'
  92           reference: __pet_ref_5
  93           read: 1
  94           write: 0
  95         - type: access
  96           relation: '[n] -> { S_2[x1, t] -> x2[] }'
  97           index: '[n] -> { S_2[x1, t] -> x2[] }'
  98           reference: __pet_ref_6
  99           read: 1
 100           write: 0
 101   arguments:
 102   - type: access
 103     relation: '[n] -> { S_2[x1, t] -> __pet_test_0[x1, -1 + t] : t >= 1 }'
 104     index: '[n] -> { S_2[x1, t] -> __pet_test_0[(x1), ((-1 + t) : t >= 1)] }'
 105     reference: __pet_ref_3
 106     read: 1
 107     write: 0
 108 - line: 14
 109   domain: '[n] -> { [S2[x1, t] -> [1]] : x1 <= -1 + n and x1 >= 0 and t >= 0 }'
 110   schedule: '[n] -> { S2[x1, t] -> [0, x1, 1, 2, t, 1, 0] }'
 111   body:
 112     type: expression
 113     expr:
 114       type: op
 115       operation: =
 116       arguments:
 117       - type: access
 118         relation: '[n] -> { S2[x1, t] -> s[] }'
 119         index: '[n] -> { S2[x1, t] -> s[] }'
 120         reference: __pet_ref_8
 121         read: 0
 122         write: 1
 123       - type: call
 124         name: g
 125         arguments:
 126         - type: access
 127           relation: '[n] -> { S2[x1, t] -> s[] }'
 128           index: '[n] -> { S2[x1, t] -> s[] }'
 129           reference: __pet_ref_9
 130           read: 1
 131           write: 0
 132   arguments:
 133   - type: access
 134     relation: '[n] -> { S2[x1, t] -> __pet_test_0[x1, t] }'
 135     index: '[n] -> { S2[x1, t] -> __pet_test_0[(x1), (t)] }'
 136     reference: __pet_ref_7
 137     read: 1
 138     write: 0
 139 - line: 13
 140   domain: '[n] -> { [S_4[x1, t] -> [1]] : x1 <= -1 + n and x1 >= 0 and t >= 0 }'
 141   schedule: '[n] -> { S_4[x1, t] -> [0, x1, 1, 2, t, 2] }'
 142   body:
 143     type: expression
 144     expr:
 145       type: op
 146       operation: +=
 147       arguments:
 148       - type: access
 149         relation: '[n] -> { S_4[x1, t] -> x2[] }'
 150         index: '[n] -> { S_4[x1, t] -> x2[] }'
 151         reference: __pet_ref_11
 152         read: 0
 153         write: 1
 154       - type: access
 155         relation: '[n] -> { S_4[x1, t] -> s[] }'
 156         index: '[n] -> { S_4[x1, t] -> s[] }'
 157         reference: __pet_ref_12
 158         read: 1
 159         write: 0
 160   arguments:
 161   - type: access
 162     relation: '[n] -> { S_4[x1, t] -> __pet_test_0[x1, t] }'
 163     index: '[n] -> { S_4[x1, t] -> __pet_test_0[(x1), (t)] }'
 164     reference: __pet_ref_10
 165     read: 1
 166     write: 0
 167 - line: 13
 168   domain: '[n] -> { S_6[x1] : x1 <= -1 + n and x1 >= 0 }'
 169   schedule: '[n] -> { S_6[x1] -> [0, x1, 1, 3] }'
 170   body:
 171     type: expression
 172     expr:
 173       type: op
 174       operation: kill
 175       arguments:
 176       - type: access
 177         relation: '[n] -> { S_6[x1] -> x2[] }'
 178         index: '[n] -> { S_6[x1] -> x2[] }'
 179         reference: __pet_ref_13
 180         read: 0
 181         write: 0
 182 - line: 16
 183   domain: '[n] -> { R[x1] : x1 <= -1 + n and x1 >= 0 }'
 184   schedule: '[n] -> { R[x1] -> [0, x1, 2] }'
 185   body:
 186     type: expression
 187     expr:
 188       type: call
 189       name: h
 190       arguments:
 191       - type: access
 192         relation: '[n] -> { R[x1] -> s[] }'
 193         index: '[n] -> { R[x1] -> s[] }'
 194         reference: __pet_ref_14
 195         read: 1
 196         write: 0
 197 implications:
 198 - satisfied: 1
 199   extension: '[n] -> { __pet_test_0[x1, t] -> __pet_test_0[x1, t''] : t'' <= t and
 200     x1 >= 0 and x1 <= -1 + n and t'' >= 0 }'