tests/for_while_init2.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         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: access
 159         relation: '[n] -> { S_4[x1, t] -> s[] }'
 160         index: '[n] -> { S_4[x1, t] -> s[] }'
 161         reference: __pet_ref_13
 162         read: 1
 163         write: 0
 164   arguments:
 165   - type: access
 166     relation: '[n] -> { S_4[x1, t] -> __pet_test_0[x1, t] }'
 167     index: '[n] -> { S_4[x1, t] -> __pet_test_0[(x1), (t)] }'
 168     reference: __pet_ref_11
 169     read: 1
 170     write: 0
 171 - line: 13
 172   domain: '[n] -> { S_6[x1] : x1 <= -1 + n and x1 >= 0 }'
 173   schedule: '[n] -> { S_6[x1] -> [0, x1, 1, 3] }'
 174   body:
 175     type: expression
 176     expr:
 177       type: op
 178       operation: kill
 179       arguments:
 180       - type: access
 181         relation: '[n] -> { S_6[x1] -> x2[] }'
 182         index: '[n] -> { S_6[x1] -> x2[] }'
 183         reference: __pet_ref_14
 184         read: 0
 185         write: 0
 186 - line: 16
 187   domain: '[n] -> { R[x1] : x1 <= -1 + n and x1 >= 0 }'
 188   schedule: '[n] -> { R[x1] -> [0, x1, 2] }'
 189   body:
 190     type: expression
 191     expr:
 192       type: call
 193       name: h
 194       arguments:
 195       - type: access
 196         relation: '[n] -> { R[x1] -> s[] }'
 197         index: '[n] -> { R[x1] -> s[] }'
 198         reference: __pet_ref_15
 199         read: 1
 200         write: 0
 201 implications:
 202 - satisfied: 1
 203   extension: '[n] -> { __pet_test_0[x1, t] -> __pet_test_0[x1, t''] : t'' <= t and
 204     x1 >= 0 and x1 <= -1 + n and t'' >= 0 }'