tests/while_break2.scop

   1 start: 45
   2 end: 157
   3 indent: "\t"
   4 context: '[N] -> {  : N <= 2147483647 and N >= -2147483648 }'
   5 schedule: '{ domain: "[N] -> { S_1[i, t] : N = 0 and i <= 9 and i >= 0 and t >= 0;
   6   S_1[0, t] : (N <= -1 and t >= 0) or (N >= 1 and t >= 0); S_0[i, t] : N = 0 and i
   7   <= 9 and i >= 0 and t >= 0; S_0[0, t] : (N <= -1 and t >= 0) or (N >= 1 and t >=
   8   0); S_2[i] : N = 0 and i <= 9 and i >= 0 }", child: { schedule: "[N] -> L_0[{ S_1[i,
   9   t] -> [(i)]; S_0[i, t] -> [(i)]; S_2[i] -> [(i)] }]", child: { sequence: [ { filter:
  10   "[N] -> { S_1[i, t]; S_0[i, t] }", child: { schedule: "[N] -> L_1[{ S_1[i, t] ->
  11   [(t)]; S_0[i, t] -> [(t)] }]", child: { sequence: [ { filter: "[N] -> { S_0[i, t]
  12   }" }, { filter: "[N] -> { S_1[i, t] }" } ] } } }, { filter: "[N] -> { S_2[i] }"
  13   } ] } } }'
  14 arrays:
  15 - context: '{  :  }'
  16   extent: '[N] -> { __pet_test_0[i, t] : N = 0 and i <= 9 and i >= 0 and t >= 0; __pet_test_0[0,
  17     t] : (N <= -1 and t >= 0) or (N >= 1 and t >= 0) }'
  18   value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
  19   element_type: int
  20   element_size: 4
  21   uniquely_defined: 1
  22 - context: '{  :  }'
  23   extent: '[N] -> { a[] }'
  24   element_type: int
  25   element_size: 4
  26 statements:
  27 - line: 10
  28   domain: '[N] -> { [S_0[i, t] -> [1]] : N = 0 and i <= 9 and i >= 0 and t >= 0; [S_0[0,
  29     t] -> [1]] : (N <= -1 and t >= 0) or (N >= 1 and t >= 0) }'
  30   body:
  31     type: expression
  32     expr:
  33       type: op
  34       operation: =
  35       arguments:
  36       - type: access
  37         index: '[N] -> { S_0[i, t] -> __pet_test_0[(i), (t)] }'
  38         reference: __pet_ref_1
  39         read: 0
  40         write: 1
  41       - type: call
  42         name: f
  43   arguments:
  44   - type: access
  45     index: '[N] -> { S_0[i, t] -> __pet_test_0[(i), ((-1 + t) : t >= 1)] }'
  46     reference: __pet_ref_0
  47     read: 1
  48     write: 0
  49 - line: 11
  50   domain: '[N] -> { [S_1[i, t] -> [1]] : N = 0 and i <= 9 and i >= 0 and t >= 0; [S_1[0,
  51     t] -> [1]] : (N <= -1 and t >= 0) or (N >= 1 and t >= 0) }'
  52   body:
  53     type: expression
  54     expr:
  55       type: op
  56       operation: =
  57       arguments:
  58       - type: access
  59         index: '[N] -> { S_1[i, t] -> a[] }'
  60         reference: __pet_ref_3
  61         read: 0
  62         write: 1
  63       - type: int
  64         value: 5
  65   arguments:
  66   - type: access
  67     index: '[N] -> { S_1[i, t] -> __pet_test_0[(i), (t)] }'
  68     reference: __pet_ref_2
  69     read: 1
  70     write: 0
  71 - line: 14
  72   domain: '[N] -> { S_2[i] : N = 0 and i <= 9 and i >= 0 }'
  73   body:
  74     type: expression
  75     expr:
  76       type: op
  77       operation: =
  78       arguments:
  79       - type: access
  80         index: '[N] -> { S_2[i] -> a[] }'
  81         reference: __pet_ref_4
  82         read: 0
  83         write: 1
  84       - type: int
  85         value: 6
  86 implications:
  87 - satisfied: 1
  88   extension: '[N] -> { __pet_test_0[i, t] -> __pet_test_0[i, t''] : N = 0 and t''
  89     <= t and i >= 0 and i <= 9 and t'' >= 0; __pet_test_0[0, t] -> __pet_test_0[0,
  90     t''] : (N >= 1 and t'' >= 0 and t'' <= t) or (N <= -1 and t'' >= 0 and t'' <=
  91     t) }'