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