tests/while_break.scop

   1 start: 45
   2 end: 294
   3 indent: "\t"
   4 context: '[N] -> {  : -2147483648 <= N <= 2147483647 }'
   5 schedule: '{ domain: "[N] -> { S_11[t] : t >= 0; S_3[t] : t >= 0; S_8[t] : t >= 0;
   6   S_10[t] : t >= 0; S_12[]; S_4[t] : t >= 0; S_6[t] : N = 0 and t >= 0; S_6[t = 0]
   7   : N < 0 or N > 0; S_7[t] : N = 0 and t >= 0; S_1[t] : N = 0 and t >= 0; S_5[t] :
   8   N = 0 and t >= 0; S_5[t = 0] : N < 0 or N > 0; S_9[t] : t >= 0; S_2[t] : t >= 0;
   9   S_0[t] : N = 0 and t >= 0; S_0[t = 0] : N < 0 or N > 0 }", child: { sequence: [
  10   { filter: "[N] -> { S_1[t]; S_0[t] }", child: { schedule: "[N] -> L_0[{ S_1[t] ->
  11   [(t)]; S_0[t] -> [(t)] }]", child: { sequence: [ { filter: "[N] -> { S_0[t] }" },
  12   { filter: "[N] -> { S_1[t] }" } ] } } }, { filter: "[N] -> { S_3[t]; S_4[t]; S_2[t]
  13   }", child: { schedule: "L_1[{ S_4[t] -> [(t)]; S_2[t] -> [(t)]; S_3[t] -> [(t)]
  14   }]", child: { sequence: [ { filter: "{ S_2[t] }" }, { filter: "{ S_3[t] }" }, {
  15   filter: "{ S_4[t] }" } ] } } }, { filter: "[N] -> { S_6[t]; S_7[t]; S_5[t] }", child:
  16   { schedule: "[N] -> L_2[{ S_6[t] -> [(t)]; S_7[t] -> [(t)]; S_5[t] -> [(t)] }]",
  17   child: { sequence: [ { filter: "[N] -> { S_5[t] }" }, { filter: "[N] -> { S_6[t]
  18   }" }, { filter: "[N] -> { S_7[t] }" } ] } } }, { filter: "[N] -> { S_11[t]; S_8[t];
  19   S_10[t]; S_9[t] }", child: { schedule: "L_3[{ S_9[t] -> [(t)]; S_10[t] -> [(t)];
  20   S_8[t] -> [(t)]; S_11[t] -> [(t)] }]", child: { sequence: [ { filter: "{ S_8[t]
  21   }" }, { filter: "{ S_9[t] }" }, { filter: "{ S_10[t] }" }, { filter: "{ S_11[t]
  22   }" } ] } } }, { filter: "[N] -> { S_12[] }" } ] } }'
  23 arrays:
  24 - context: '{  :  }'
  25   extent: '[N] -> { __pet_test_0[t] : t >= 0 }'
  26   value_bounds: '{ [i0] : 0 <= i0 <= 1 }'
  27   element_type: int
  28   element_size: 4
  29   uniquely_defined: 1
  30 - context: '{  :  }'
  31   extent: '[N] -> { __pet_test_1[t] : N = 0 and t >= 0; __pet_test_1[t = 0] : N <
  32     0 or N > 0 }'
  33   value_bounds: '{ [i0] : 0 <= i0 <= 1 }'
  34   element_type: int
  35   element_size: 4
  36   uniquely_defined: 1
  37 - context: '{  :  }'
  38   extent: '[N] -> { __pet_test_2[t] : t >= 0 }'
  39   value_bounds: '{ [i0] : 0 <= i0 <= 1 }'
  40   element_type: int
  41   element_size: 4
  42   uniquely_defined: 1
  43 - context: '{  :  }'
  44   extent: '[N] -> { __pet_test_3[t] : t >= 0 }'
  45   value_bounds: '{ [i0] : 0 <= i0 <= 1 }'
  46   element_type: int
  47   element_size: 4
  48   uniquely_defined: 1
  49 - context: '{  :  }'
  50   extent: '[N] -> { a[] }'
  51   element_type: int
  52   element_size: 4
  53 statements:
  54 - line: 10
  55   domain: '[N] -> { S_0[t] : N = 0 and t >= 0; S_0[t = 0] : N < 0 or N > 0 }'
  56   body:
  57     type: expression
  58     expr:
  59       type: op
  60       operation: =
  61       arguments:
  62       - type: access
  63         index: '[N] -> { S_0[t] -> a[] }'
  64         reference: __pet_ref_0
  65         read: 0
  66         write: 1
  67       - type: int
  68         value: 5
  69 - line: 13
  70   domain: '[N] -> { S_1[t] : N = 0 and t >= 0 }'
  71   body:
  72     type: expression
  73     expr:
  74       type: op
  75       operation: =
  76       arguments:
  77       - type: access
  78         index: '[N] -> { S_1[t] -> a[] }'
  79         reference: __pet_ref_1
  80         read: 0
  81         write: 1
  82       - type: int
  83         value: 6
  84 - line: 16
  85   domain: '[N] -> { [S_2[t] -> [__pet_test_0 = 0]] : t >= 0 }'
  86   body:
  87     type: expression
  88     expr:
  89       type: op
  90       operation: =
  91       arguments:
  92       - type: access
  93         index: '[N] -> { S_2[t] -> a[] }'
  94         reference: __pet_ref_3
  95         read: 0
  96         write: 1
  97       - type: int
  98         value: 5
  99   arguments:
 100   - type: access
 101     index: '[N] -> { S_2[t] -> __pet_test_0[((-1 + t) : t > 0)] }'
 102     reference: __pet_ref_2
 103     read: 1
 104     write: 0
 105 - line: 17
 106   domain: '[N] -> { [S_3[t] -> [__pet_test_0 = 0]] : t >= 0 }'
 107   body:
 108     type: expression
 109     expr:
 110       type: op
 111       operation: =
 112       arguments:
 113       - type: access
 114         index: '[N] -> { S_3[t] -> __pet_test_0[(t)] }'
 115         reference: __pet_ref_5
 116         read: 0
 117         write: 1
 118       - type: call
 119         name: f
 120   arguments:
 121   - type: access
 122     index: '[N] -> { S_3[t] -> __pet_test_0[((-1 + t) : t > 0)] }'
 123     reference: __pet_ref_4
 124     read: 1
 125     write: 0
 126 - line: 19
 127   domain: '[N] -> { [S_4[t] -> [__pet_test_0 = 0]] : t >= 0 }'
 128   body:
 129     type: expression
 130     expr:
 131       type: op
 132       operation: =
 133       arguments:
 134       - type: access
 135         index: '[N] -> { S_4[t] -> a[] }'
 136         reference: __pet_ref_7
 137         read: 0
 138         write: 1
 139       - type: int
 140         value: 6
 141   arguments:
 142   - type: access
 143     index: '[N] -> { S_4[t] -> __pet_test_0[(t)] }'
 144     reference: __pet_ref_6
 145     read: 1
 146     write: 0
 147 - line: 21
 148   domain: '[N] -> { [S_5[t] -> [__pet_test_1 = 1]] : N = 0 and t >= 0; [S_5[t = 0]
 149     -> [__pet_test_1 = 1]] : N < 0 or N > 0 }'
 150   body:
 151     type: expression
 152     expr:
 153       type: op
 154       operation: =
 155       arguments:
 156       - type: access
 157         index: '[N] -> { S_5[t] -> __pet_test_1[(t)] }'
 158         reference: __pet_ref_9
 159         read: 0
 160         write: 1
 161       - type: call
 162         name: f
 163   arguments:
 164   - type: access
 165     index: '[N] -> { S_5[t] -> __pet_test_1[((-1 + t) : (t = 1 and N < 0) or (t =
 166       1 and N > 0) or (N = 0 and t > 0))] }'
 167     reference: __pet_ref_8
 168     read: 1
 169     write: 0
 170 - line: 22
 171   domain: '[N] -> { [S_6[t] -> [__pet_test_1 = 1]] : N = 0 and t >= 0; [S_6[t = 0]
 172     -> [__pet_test_1 = 1]] : N < 0 or N > 0 }'
 173   body:
 174     type: expression
 175     expr:
 176       type: op
 177       operation: =
 178       arguments:
 179       - type: access
 180         index: '[N] -> { S_6[t] -> a[] }'
 181         reference: __pet_ref_11
 182         read: 0
 183         write: 1
 184       - type: int
 185         value: 5
 186   arguments:
 187   - type: access
 188     index: '[N] -> { S_6[t] -> __pet_test_1[(t)] }'
 189     reference: __pet_ref_10
 190     read: 1
 191     write: 0
 192 - line: 25
 193   domain: '[N] -> { [S_7[t] -> [__pet_test_1 = 1]] : N = 0 and t >= 0 }'
 194   body:
 195     type: expression
 196     expr:
 197       type: op
 198       operation: =
 199       arguments:
 200       - type: access
 201         index: '[N] -> { S_7[t] -> a[] }'
 202         reference: __pet_ref_13
 203         read: 0
 204         write: 1
 205       - type: int
 206         value: 6
 207   arguments:
 208   - type: access
 209     index: '[N] -> { S_7[t] -> __pet_test_1[(t)] }'
 210     reference: __pet_ref_12
 211     read: 1
 212     write: 0
 213 - line: 27
 214   domain: '[N] -> { [S_8[t] -> [__pet_test_2 = 1, __pet_test_3 = 0]] : t >= 0 }'
 215   body:
 216     type: expression
 217     expr:
 218       type: op
 219       operation: =
 220       arguments:
 221       - type: access
 222         index: '[N] -> { S_8[t] -> __pet_test_2[(t)] }'
 223         reference: __pet_ref_16
 224         read: 0
 225         write: 1
 226       - type: call
 227         name: f
 228   arguments:
 229   - type: access
 230     index: '[N] -> { S_8[t] -> __pet_test_2[((-1 + t) : t > 0)] }'
 231     reference: __pet_ref_14
 232     read: 1
 233     write: 0
 234   - type: access
 235     index: '[N] -> { S_8[t] -> __pet_test_3[((-1 + t) : t > 0)] }'
 236     reference: __pet_ref_15
 237     read: 1
 238     write: 0
 239 - line: 28
 240   domain: '[N] -> { [S_9[t] -> [__pet_test_2 = 1, __pet_test_3 = 0]] : t >= 0 }'
 241   body:
 242     type: expression
 243     expr:
 244       type: op
 245       operation: =
 246       arguments:
 247       - type: access
 248         index: '[N] -> { S_9[t] -> a[] }'
 249         reference: __pet_ref_19
 250         read: 0
 251         write: 1
 252       - type: int
 253         value: 5
 254   arguments:
 255   - type: access
 256     index: '[N] -> { S_9[t] -> __pet_test_2[(t)] }'
 257     reference: __pet_ref_17
 258     read: 1
 259     write: 0
 260   - type: access
 261     index: '[N] -> { S_9[t] -> __pet_test_3[((-1 + t) : t > 0)] }'
 262     reference: __pet_ref_18
 263     read: 1
 264     write: 0
 265 - line: 29
 266   domain: '[N] -> { [S_10[t] -> [__pet_test_2 = 1, __pet_test_3 = 0]] : t >= 0 }'
 267   body:
 268     type: expression
 269     expr:
 270       type: op
 271       operation: =
 272       arguments:
 273       - type: access
 274         index: '[N] -> { S_10[t] -> __pet_test_3[(t)] }'
 275         reference: __pet_ref_22
 276         read: 0
 277         write: 1
 278       - type: call
 279         name: f
 280   arguments:
 281   - type: access
 282     index: '[N] -> { S_10[t] -> __pet_test_2[(t)] }'
 283     reference: __pet_ref_20
 284     read: 1
 285     write: 0
 286   - type: access
 287     index: '[N] -> { S_10[t] -> __pet_test_3[((-1 + t) : t > 0)] }'
 288     reference: __pet_ref_21
 289     read: 1
 290     write: 0
 291 - line: 31
 292   domain: '[N] -> { [S_11[t] -> [__pet_test_2 = 1, __pet_test_3 = 0]] : t >= 0 }'
 293   body:
 294     type: expression
 295     expr:
 296       type: op
 297       operation: =
 298       arguments:
 299       - type: access
 300         index: '[N] -> { S_11[t] -> a[] }'
 301         reference: __pet_ref_25
 302         read: 0
 303         write: 1
 304       - type: int
 305         value: 6
 306   arguments:
 307   - type: access
 308     index: '[N] -> { S_11[t] -> __pet_test_2[(t)] }'
 309     reference: __pet_ref_23
 310     read: 1
 311     write: 0
 312   - type: access
 313     index: '[N] -> { S_11[t] -> __pet_test_3[(t)] }'
 314     reference: __pet_ref_24
 315     read: 1
 316     write: 0
 317 - line: -1
 318   domain: '[N] -> { S_12[] }'
 319   body:
 320     type: expression
 321     expr:
 322       type: op
 323       operation: kill
 324       arguments:
 325       - type: access
 326         killed: '[N] -> { S_12[] -> a[] }'
 327         index: '[N] -> { S_12[] -> a[] }'
 328         reference: __pet_ref_26
 329         kill: 1
 330 implications:
 331 - satisfied: 0
 332   extension: '{ __pet_test_0[t] -> __pet_test_0[t''] : 0 <= t'' <= t }'
 333 - satisfied: 1
 334   extension: '[N] -> { __pet_test_1[t] -> __pet_test_1[t''] : N = 0 and 0 <= t'' <=
 335     t; __pet_test_1[t] -> __pet_test_1[t'' = 0] : t >= 0 and (N > 0 or N < 0) }'
 336 - satisfied: 0
 337   extension: '{ __pet_test_3[t] -> __pet_test_3[t''] : 0 <= t'' <= t }'
 338 - satisfied: 1
 339   extension: '{ __pet_test_2[t] -> __pet_test_2[t''] : 0 <= t'' <= t }'