tests/for_while_init.scop

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