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