tests/while_break.scop

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