tests/for_while_init2.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: access
  79         index: '[n] -> { S_1[x1] -> s[] }'
  80         reference: __pet_ref_3
  81         read: 1
  82         write: 0
  83 - line: 13
  84   domain: '[n] -> { [S_2[x1, t] -> [1]] : x1 >= 0 and x1 <= -1 + n and t >= 0 }'
  85   body:
  86     type: expression
  87     expr:
  88       type: op
  89       operation: =
  90       arguments:
  91       - type: access
  92         index: '[n] -> { S_2[x1, t] -> __pet_test_0[(x1), (t)] }'
  93         reference: __pet_ref_5
  94         read: 0
  95         write: 1
  96       - type: call
  97         name: P
  98         arguments:
  99         - type: access
 100           index: '[n] -> { S_2[x1, t] -> [(x1)] }'
 101           reference: __pet_ref_6
 102           read: 1
 103           write: 0
 104         - type: access
 105           index: '[n] -> { S_2[x1, t] -> x2[] }'
 106           reference: __pet_ref_7
 107           read: 1
 108           write: 0
 109   arguments:
 110   - type: access
 111     index: '[n] -> { S_2[x1, t] -> __pet_test_0[(x1), ((-1 + t) : t >= 1)] }'
 112     reference: __pet_ref_4
 113     read: 1
 114     write: 0
 115 - line: 14
 116   domain: '[n] -> { [S2[x1, t] -> [1]] : x1 >= 0 and x1 <= -1 + n and t >= 0 }'
 117   body:
 118     type: expression
 119     expr:
 120       type: op
 121       operation: =
 122       arguments:
 123       - type: access
 124         index: '[n] -> { S2[x1, t] -> s[] }'
 125         reference: __pet_ref_9
 126         read: 0
 127         write: 1
 128       - type: call
 129         name: g
 130         arguments:
 131         - type: access
 132           index: '[n] -> { S2[x1, t] -> s[] }'
 133           reference: __pet_ref_10
 134           read: 1
 135           write: 0
 136   arguments:
 137   - type: access
 138     index: '[n] -> { S2[x1, t] -> __pet_test_0[(x1), (t)] }'
 139     reference: __pet_ref_8
 140     read: 1
 141     write: 0
 142 - line: 13
 143   domain: '[n] -> { [S_4[x1, t] -> [1]] : x1 >= 0 and x1 <= -1 + n and t >= 0 }'
 144   body:
 145     type: expression
 146     expr:
 147       type: op
 148       operation: +=
 149       arguments:
 150       - type: access
 151         index: '[n] -> { S_4[x1, t] -> x2[] }'
 152         reference: __pet_ref_12
 153         read: 0
 154         write: 1
 155       - type: access
 156         index: '[n] -> { S_4[x1, t] -> s[] }'
 157         reference: __pet_ref_13
 158         read: 1
 159         write: 0
 160   arguments:
 161   - type: access
 162     index: '[n] -> { S_4[x1, t] -> __pet_test_0[(x1), (t)] }'
 163     reference: __pet_ref_11
 164     read: 1
 165     write: 0
 166 - line: 13
 167   domain: '[n] -> { S_6[x1] : x1 >= 0 and x1 <= -1 + n }'
 168   body:
 169     type: expression
 170     expr:
 171       type: op
 172       operation: kill
 173       arguments:
 174       - type: access
 175         killed: '[n] -> { S_6[x1] -> x2[] }'
 176         index: '[n] -> { S_6[x1] -> x2[] }'
 177         reference: __pet_ref_14
 178         kill: 1
 179 - line: 16
 180   domain: '[n] -> { R[x1] : x1 >= 0 and x1 <= -1 + n }'
 181   body:
 182     type: expression
 183     expr:
 184       type: call
 185       name: h
 186       arguments:
 187       - type: access
 188         index: '[n] -> { R[x1] -> s[] }'
 189         reference: __pet_ref_15
 190         read: 1
 191         write: 0
 192 - line: -1
 193   domain: '[n] -> { S_8[] }'
 194   body:
 195     type: expression
 196     expr:
 197       type: op
 198       operation: kill
 199       arguments:
 200       - type: access
 201         killed: '[n] -> { S_8[] -> s[] }'
 202         index: '[n] -> { S_8[] -> s[] }'
 203         reference: __pet_ref_16
 204         kill: 1
 205 implications:
 206 - satisfied: 1
 207   extension: '[n] -> { __pet_test_0[x1, t] -> __pet_test_0[x1, t''] : t'' <= t and
 208     x1 >= 0 and x1 <= -1 + n and t'' >= 0 }'