tests/for_while_inc3.scop

   1 start: 83
   2 end: 234
   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: int
  63       value: 0
  64 - line: 13
  65   domain: '[n] -> { [S_2[x1, t] -> [1]] : x1 <= -1 + n and x1 >= 0 and t >= 0 }'
  66   schedule: '[n] -> { S_2[x1, t] -> [0, x1, 1, 2, t, 0] }'
  67   body:
  68     type: op
  69     operation: =
  70     arguments:
  71     - type: access
  72       relation: '[n] -> { S_2[x1, t] -> __pet_test_0[x1, t] }'
  73       index: '[n] -> { S_2[x1, t] -> __pet_test_0[(x1), (t)] }'
  74       reference: __pet_ref_4
  75       read: 0
  76       write: 1
  77     - type: call
  78       name: P
  79       arguments:
  80       - type: access
  81         relation: '[n] -> { S_2[x1, t] -> [x1] }'
  82         index: '[n] -> { S_2[x1, t] -> [(x1)] }'
  83         reference: __pet_ref_5
  84         read: 1
  85         write: 0
  86       - type: access
  87         relation: '[n] -> { S_2[x1, t] -> x2[] }'
  88         index: '[n] -> { S_2[x1, t] -> x2[] }'
  89         reference: __pet_ref_6
  90         read: 1
  91         write: 0
  92   arguments:
  93   - type: access
  94     relation: '[n] -> { S_2[x1, t] -> __pet_test_0[x1, -1 + t] : t >= 1 }'
  95     index: '[n] -> { S_2[x1, t] -> __pet_test_0[(x1), ((-1 + t) : t >= 1)] }'
  96     reference: __pet_ref_3
  97     read: 1
  98     write: 0
  99 - line: 14
 100   domain: '[n] -> { [S2[x1, t] -> [1]] : x1 <= -1 + n and x1 >= 0 and t >= 0 }'
 101   schedule: '[n] -> { S2[x1, t] -> [0, x1, 1, 2, t, 1, 0] }'
 102   body:
 103     type: op
 104     operation: =
 105     arguments:
 106     - type: access
 107       relation: '[n] -> { S2[x1, t] -> s[] }'
 108       index: '[n] -> { S2[x1, t] -> s[] }'
 109       reference: __pet_ref_8
 110       read: 0
 111       write: 1
 112     - type: call
 113       name: g
 114       arguments:
 115       - type: access
 116         relation: '[n] -> { S2[x1, t] -> s[] }'
 117         index: '[n] -> { S2[x1, t] -> s[] }'
 118         reference: __pet_ref_9
 119         read: 1
 120         write: 0
 121   arguments:
 122   - type: access
 123     relation: '[n] -> { S2[x1, t] -> __pet_test_0[x1, t] }'
 124     index: '[n] -> { S2[x1, t] -> __pet_test_0[(x1), (t)] }'
 125     reference: __pet_ref_7
 126     read: 1
 127     write: 0
 128 - line: 13
 129   domain: '[n] -> { [S_4[x1, t] -> [1]] : x1 <= -1 + n and x1 >= 0 and t >= 0 }'
 130   schedule: '[n] -> { S_4[x1, t] -> [0, x1, 1, 2, t, 2] }'
 131   body:
 132     type: op
 133     operation: +=
 134     arguments:
 135     - type: access
 136       relation: '[n] -> { S_4[x1, t] -> x2[] }'
 137       index: '[n] -> { S_4[x1, t] -> x2[] }'
 138       reference: __pet_ref_11
 139       read: 0
 140       write: 1
 141     - type: access
 142       relation: '[n] -> { S_4[x1, t] -> [n] }'
 143       index: '[n] -> { S_4[x1, t] -> [(n)] }'
 144       reference: __pet_ref_12
 145       read: 1
 146       write: 0
 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_10
 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 }'