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