tests/for_while_init.scop

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