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