tests/while_break2.scop

   1 start: 45
   2 end: 157
   3 indent: "\t"
   4 context: '[N] -> {  : -2147483648 <= N <= 2147483647 }'
   5 schedule: '{ domain: "[N] -> { S_3[i] : N = 0 and 0 <= i <= 9; S_5[]; S_2[i, t] :
   6   N = 0 and 0 <= i <= 9 and t >= 0; S_2[i = 0, t] : t >= 0 and (N < 0 or N > 0); S_6[];
   7   S_1[i, t] : N = 0 and 0 <= i <= 9 and t >= 0; S_1[i = 0, t] : t >= 0 and (N < 0
   8   or N > 0); S_4[i] : N = 0 and 0 <= i <= 9; S_0[] }", child: { sequence: [ { filter:
   9   "[N] -> { S_0[] }" }, { filter: "[N] -> { S_3[i]; S_2[i, t]; S_1[i, t]; S_4[i] }",
  10   child: { schedule: "[N] -> L_0[{ S_3[i] -> [(i)]; S_2[i, t] -> [(i)]; S_1[i, t]
  11   -> [(i)]; S_4[i] -> [(i)] }]", child: { sequence: [ { filter: "[N] -> { S_2[i, t];
  12   S_1[i, t] }", child: { schedule: "[N] -> L_1[{ S_2[i, t] -> [(t)]; S_1[i, t] ->
  13   [(t)] }]", child: { sequence: [ { filter: "[N] -> { S_1[i, t] }" }, { filter: "[N]
  14   -> { S_2[i, t] }" } ] } } }, { filter: "[N] -> { S_3[i] }" }, { filter: "[N] ->
  15   { S_4[i] }" } ] } } }, { filter: "[N] -> { S_5[]; S_6[] }", child: { set: [ { filter:
  16   "{ S_5[] }" }, { filter: "{ S_6[] }" } ] } } ] } }'
  17 arrays:
  18 - context: '{  :  }'
  19   extent: '[N] -> { __pet_test_0[i, t] : N = 0 and 0 <= i <= 9 and t >= 0; __pet_test_0[i
  20     = 0, t] : t >= 0 and (N < 0 or N > 0) }'
  21   value_bounds: '{ [i0] : 0 <= i0 <= 1 }'
  22   element_type: int
  23   element_size: 4
  24   uniquely_defined: 1
  25 - context: '{  :  }'
  26   extent: '[N] -> { a[] }'
  27   element_type: int
  28   element_size: 4
  29 - context: '{  :  }'
  30   extent: '[N] -> { i[] }'
  31   element_type: int
  32   element_size: 4
  33 statements:
  34 - line: 9
  35   domain: '[N] -> { S_0[] }'
  36   body:
  37     type: expression
  38     expr:
  39       type: op
  40       operation: =
  41       arguments:
  42       - type: access
  43         index: '[N] -> { S_0[] -> i[] }'
  44         reference: __pet_ref_0
  45         read: 0
  46         write: 1
  47       - type: int
  48         value: 0
  49 - line: 10
  50   domain: '[N] -> { [S_1[i, t] -> [__pet_test_0 = 1]] : N = 0 and 0 <= i <= 9 and
  51     t >= 0; [S_1[i = 0, t] -> [__pet_test_0 = 1]] : t >= 0 and (N < 0 or N > 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] -> __pet_test_0[(i), (t)] }'
  60         reference: __pet_ref_2
  61         read: 0
  62         write: 1
  63       - type: call
  64         name: f
  65   arguments:
  66   - type: access
  67     index: '[N] -> { S_1[i, t] -> __pet_test_0[(i), ((-1 + t) : t > 0)] }'
  68     reference: __pet_ref_1
  69     read: 1
  70     write: 0
  71 - line: 11
  72   domain: '[N] -> { [S_2[i, t] -> [__pet_test_0 = 1]] : N = 0 and 0 <= i <= 9 and
  73     t >= 0; [S_2[i = 0, t] -> [__pet_test_0 = 1]] : t >= 0 and (N < 0 or N > 0) }'
  74   body:
  75     type: expression
  76     expr:
  77       type: op
  78       operation: =
  79       arguments:
  80       - type: access
  81         index: '[N] -> { S_2[i, t] -> a[] }'
  82         reference: __pet_ref_4
  83         read: 0
  84         write: 1
  85       - type: int
  86         value: 5
  87   arguments:
  88   - type: access
  89     index: '[N] -> { S_2[i, t] -> __pet_test_0[(i), (t)] }'
  90     reference: __pet_ref_3
  91     read: 1
  92     write: 0
  93 - line: 14
  94   domain: '[N] -> { S_3[i] : N = 0 and 0 <= i <= 9 }'
  95   body:
  96     type: expression
  97     expr:
  98       type: op
  99       operation: =
 100       arguments:
 101       - type: access
 102         index: '[N] -> { S_3[i] -> a[] }'
 103         reference: __pet_ref_5
 104         read: 0
 105         write: 1
 106       - type: int
 107         value: 6
 108 - line: 9
 109   domain: '[N] -> { S_4[i] : N = 0 and 0 <= i <= 9 }'
 110   body:
 111     type: expression
 112     expr:
 113       type: op
 114       operation: =
 115       arguments:
 116       - type: access
 117         index: '[N] -> { S_4[i] -> i[] }'
 118         reference: __pet_ref_6
 119         read: 0
 120         write: 1
 121       - type: access
 122         index: '[N] -> { S_4[i] -> [(1 + i)] }'
 123         reference: __pet_ref_7
 124         read: 1
 125         write: 0
 126 - line: -1
 127   domain: '[N] -> { S_5[] }'
 128   body:
 129     type: expression
 130     expr:
 131       type: op
 132       operation: kill
 133       arguments:
 134       - type: access
 135         killed: '[N] -> { S_5[] -> i[] }'
 136         index: '[N] -> { S_5[] -> i[] }'
 137         reference: __pet_ref_8
 138         kill: 1
 139 - line: -1
 140   domain: '[N] -> { S_6[] }'
 141   body:
 142     type: expression
 143     expr:
 144       type: op
 145       operation: kill
 146       arguments:
 147       - type: access
 148         killed: '[N] -> { S_6[] -> a[] }'
 149         index: '[N] -> { S_6[] -> a[] }'
 150         reference: __pet_ref_9
 151         kill: 1
 152 implications:
 153 - satisfied: 1
 154   extension: '[N] -> { __pet_test_0[i, t] -> __pet_test_0[i'' = i, t''] : N = 0 and
 155     0 <= i <= 9 and 0 <= t'' <= t; __pet_test_0[i = 0, t] -> __pet_test_0[i'' = 0,
 156     t''] : 0 <= t'' <= t and (N > 0 or N < 0) }'