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