tests/for_while_inc4.scop

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