tests/for_while_inc3.scop

   1 start: 83
   2 end: 234
   3 indent: "\t"
   4 context: '[n] -> {  : n <= 2147483647 and n >= -2147483648 }'
   5 schedule: '{ domain: "[n] -> { S_6[x1] : x1 >= 0 and x1 <= -1 + n; S_2[x1, t] : x1
   6   >= 0 and x1 <= -1 + n and t >= 0; S2[x1, t] : x1 >= 0 and x1 <= -1 + n and t >=
   7   0; S1[x1] : x1 >= 0 and x1 <= -1 + n; S_5[x1] : x1 >= 0 and x1 <= -1 + n; S_1[x1]
   8   : x1 >= 0 and x1 <= -1 + n; R[x1] : x1 >= 0 and x1 <= -1 + n; S_4[x1, t] : x1 >=
   9   0 and x1 <= -1 + n and t >= 0 }", child: { schedule: "[n] -> L_0[{ S_6[x1] -> [(x1)];
  10   S_2[x1, t] -> [(x1)]; S2[x1, t] -> [(x1)]; S1[x1] -> [(x1)]; S_5[x1] -> [(x1)];
  11   S_1[x1] -> [(x1)]; R[x1] -> [(x1)]; S_4[x1, t] -> [(x1)] }]", child: { sequence:
  12   [ { filter: "[n] -> { S1[x1] }" }, { filter: "[n] -> { S_5[x1] }" }, { filter: "[n]
  13   -> { S_1[x1] }" }, { filter: "[n] -> { S_2[x1, t]; S2[x1, t]; S_4[x1, t] }", child:
  14   { schedule: "[n] -> L_1[{ S_2[x1, t] -> [(t)]; S2[x1, t] -> [(t)]; S_4[x1, t] ->
  15   [(t)] }]", child: { sequence: [ { filter: "[n] -> { S_2[x1, t] }" }, { filter: "[n]
  16   -> { S2[x1, t] }" }, { filter: "[n] -> { S_4[x1, t] }" } ] } } }, { filter: "[n]
  17   -> { S_6[x1] }" }, { filter: "[n] -> { R[x1] }" } ] } } }'
  18 arrays:
  19 - context: '{  :  }'
  20   extent: '[n] -> { __pet_test_0[x1, t] : x1 >= 0 and x1 <= -1 + n and t >= 0 }'
  21   value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
  22   element_type: int
  23   element_size: 4
  24   uniquely_defined: 1
  25 - context: '{  :  }'
  26   extent: '[n] -> { x2[] }'
  27   element_type: int
  28   element_size: 4
  29   declared: 1
  30 - context: '{  :  }'
  31   extent: '[n] -> { s[] }'
  32   element_type: int
  33   element_size: 4
  34 statements:
  35 - line: 12
  36   domain: '[n] -> { S1[x1] : x1 >= 0 and x1 <= -1 + n }'
  37   body:
  38     type: expression
  39     expr:
  40       type: op
  41       operation: =
  42       arguments:
  43       - type: access
  44         index: '[n] -> { S1[x1] -> s[] }'
  45         reference: __pet_ref_0
  46         read: 0
  47         write: 1
  48       - type: call
  49         name: f
  50 - line: 13
  51   domain: '[n] -> { S_5[x1] : x1 >= 0 and x1 <= -1 + n }'
  52   body:
  53     type: expression
  54     expr:
  55       type: op
  56       operation: kill
  57       arguments:
  58       - type: access
  59         killed: '[n] -> { S_5[x1] -> x2[] }'
  60         index: '[n] -> { S_5[x1] -> x2[] }'
  61         reference: __pet_ref_1
  62         kill: 1
  63 - line: 13
  64   domain: '[n] -> { S_1[x1] : x1 >= 0 and x1 <= -1 + n }'
  65   body:
  66     type: expression
  67     expr:
  68       type: op
  69       operation: =
  70       arguments:
  71       - type: access
  72         index: '[n] -> { S_1[x1] -> x2[] }'
  73         reference: __pet_ref_2
  74         read: 0
  75         write: 1
  76       - type: int
  77         value: 0
  78 - line: 13
  79   domain: '[n] -> { [S_2[x1, t] -> [1]] : x1 >= 0 and x1 <= -1 + n and t >= 0 }'
  80   body:
  81     type: expression
  82     expr:
  83       type: op
  84       operation: =
  85       arguments:
  86       - type: access
  87         index: '[n] -> { S_2[x1, t] -> __pet_test_0[(x1), (t)] }'
  88         reference: __pet_ref_4
  89         read: 0
  90         write: 1
  91       - type: call
  92         name: P
  93         arguments:
  94         - type: access
  95           index: '[n] -> { S_2[x1, t] -> [(x1)] }'
  96           reference: __pet_ref_5
  97           read: 1
  98           write: 0
  99         - type: access
 100           index: '[n] -> { S_2[x1, t] -> x2[] }'
 101           reference: __pet_ref_6
 102           read: 1
 103           write: 0
 104   arguments:
 105   - type: access
 106     index: '[n] -> { S_2[x1, t] -> __pet_test_0[(x1), ((-1 + t) : t >= 1)] }'
 107     reference: __pet_ref_3
 108     read: 1
 109     write: 0
 110 - line: 14
 111   domain: '[n] -> { [S2[x1, t] -> [1]] : x1 >= 0 and x1 <= -1 + n and t >= 0 }'
 112   body:
 113     type: expression
 114     expr:
 115       type: op
 116       operation: =
 117       arguments:
 118       - type: access
 119         index: '[n] -> { S2[x1, t] -> s[] }'
 120         reference: __pet_ref_8
 121         read: 0
 122         write: 1
 123       - type: call
 124         name: g
 125         arguments:
 126         - type: access
 127           index: '[n] -> { S2[x1, t] -> s[] }'
 128           reference: __pet_ref_9
 129           read: 1
 130           write: 0
 131   arguments:
 132   - type: access
 133     index: '[n] -> { S2[x1, t] -> __pet_test_0[(x1), (t)] }'
 134     reference: __pet_ref_7
 135     read: 1
 136     write: 0
 137 - line: 13
 138   domain: '[n] -> { [S_4[x1, t] -> [1]] : x1 >= 0 and x1 <= -1 + n and t >= 0 }'
 139   body:
 140     type: expression
 141     expr:
 142       type: op
 143       operation: +=
 144       arguments:
 145       - type: access
 146         index: '[n] -> { S_4[x1, t] -> x2[] }'
 147         reference: __pet_ref_11
 148         read: 0
 149         write: 1
 150       - type: access
 151         index: '[n] -> { S_4[x1, t] -> [(n)] }'
 152         reference: __pet_ref_12
 153         read: 1
 154         write: 0
 155   arguments:
 156   - type: access
 157     index: '[n] -> { S_4[x1, t] -> __pet_test_0[(x1), (t)] }'
 158     reference: __pet_ref_10
 159     read: 1
 160     write: 0
 161 - line: 13
 162   domain: '[n] -> { S_6[x1] : x1 >= 0 and x1 <= -1 + n }'
 163   body:
 164     type: expression
 165     expr:
 166       type: op
 167       operation: kill
 168       arguments:
 169       - type: access
 170         killed: '[n] -> { S_6[x1] -> x2[] }'
 171         index: '[n] -> { S_6[x1] -> x2[] }'
 172         reference: __pet_ref_13
 173         kill: 1
 174 - line: 16
 175   domain: '[n] -> { R[x1] : x1 >= 0 and x1 <= -1 + n }'
 176   body:
 177     type: expression
 178     expr:
 179       type: call
 180       name: h
 181       arguments:
 182       - type: access
 183         index: '[n] -> { R[x1] -> s[] }'
 184         reference: __pet_ref_14
 185         read: 1
 186         write: 0
 187 implications:
 188 - satisfied: 1
 189   extension: '[n] -> { __pet_test_0[x1, t] -> __pet_test_0[x1, t''] : t'' <= t and
 190     x1 >= 0 and x1 <= -1 + n and t'' >= 0 }'