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[-1 + t] : t >= 1 }'
  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[-1 + t] : t >= 1 }'
 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[t] }'
 131     reference: __pet_ref_9
 132     read: 1
 133     write: 0
 134 - line: 21
 135   domain: '[N] -> { [S_5[t] -> [1]] : N = 0 and t >= 1; [S_5[0] -> [1]] }'
 136   schedule: '[N] -> { S_5[t] -> [2, t, 0] }'
 137   body:
 138     type: binary
 139     operation: =
 140     arguments:
 141     - type: access
 142       relation: '[N] -> { S_5[t] -> __pet_test_1[t] }'
 143       reference: __pet_ref_13
 144       read: 0
 145       write: 1
 146     - type: call
 147       name: f
 148   arguments:
 149   - type: access
 150     relation: '[N] -> { S_5[t] -> __pet_test_1[-1 + t] : N = 0 and t >= 2; S_5[1]
 151       -> __pet_test_1[0] }'
 152     reference: __pet_ref_12
 153     read: 1
 154     write: 0
 155 - line: 22
 156   domain: '[N] -> { [S_6[t] -> [1]] : N = 0 and t >= 1; [S_6[0] -> [1]] }'
 157   schedule: '[N] -> { S_6[t] -> [2, t, 1, 0] }'
 158   body:
 159     type: binary
 160     operation: =
 161     arguments:
 162     - type: access
 163       relation: '[N] -> { S_6[t] -> a[] }'
 164       reference: __pet_ref_15
 165       read: 0
 166       write: 1
 167     - type: access
 168       relation: '[N] -> { S_6[t] -> [5] }'
 169       reference: __pet_ref_16
 170       read: 1
 171       write: 0
 172   arguments:
 173   - type: access
 174     relation: '[N] -> { S_6[t] -> __pet_test_1[t] }'
 175     reference: __pet_ref_14
 176     read: 1
 177     write: 0
 178 - line: 25
 179   domain: '[N] -> { [S_7[t] -> [1]] : N = 0 and t >= 1; [S_7[0] -> [1]] : N = 0 }'
 180   schedule: '[N] -> { S_7[t] -> [2, t, 1, 2] }'
 181   body:
 182     type: binary
 183     operation: =
 184     arguments:
 185     - type: access
 186       relation: '[N] -> { S_7[t] -> a[] }'
 187       reference: __pet_ref_18
 188       read: 0
 189       write: 1
 190     - type: access
 191       relation: '[N] -> { S_7[t] -> [6] }'
 192       reference: __pet_ref_19
 193       read: 1
 194       write: 0
 195   arguments:
 196   - type: access
 197     relation: '[N] -> { S_7[t] -> __pet_test_1[t] }'
 198     reference: __pet_ref_17
 199     read: 1
 200     write: 0
 201 - line: 27
 202   domain: '[N] -> { [S_8[t] -> [1, 0]] : t >= 0 }'
 203   schedule: '{ S_8[t] -> [3, t, 0] }'
 204   body:
 205     type: binary
 206     operation: =
 207     arguments:
 208     - type: access
 209       relation: '[N] -> { S_8[t] -> __pet_test_2[t] }'
 210       reference: __pet_ref_22
 211       read: 0
 212       write: 1
 213     - type: call
 214       name: f
 215   arguments:
 216   - type: access
 217     relation: '[N] -> { S_8[t] -> __pet_test_2[-1 + t] : t >= 1 }'
 218     reference: __pet_ref_20
 219     read: 1
 220     write: 0
 221   - type: access
 222     relation: '[N] -> { S_8[t] -> __pet_test_3[-1 + t] : t >= 1 }'
 223     reference: __pet_ref_21
 224     read: 1
 225     write: 0
 226 - line: 28
 227   domain: '[N] -> { [S_9[t] -> [1, 0]] : t >= 0 }'
 228   schedule: '{ S_9[t] -> [3, t, 1, 0] }'
 229   body:
 230     type: binary
 231     operation: =
 232     arguments:
 233     - type: access
 234       relation: '[N] -> { S_9[t] -> a[] }'
 235       reference: __pet_ref_25
 236       read: 0
 237       write: 1
 238     - type: access
 239       relation: '[N] -> { S_9[t] -> [5] }'
 240       reference: __pet_ref_26
 241       read: 1
 242       write: 0
 243   arguments:
 244   - type: access
 245     relation: '[N] -> { S_9[t] -> __pet_test_2[t] }'
 246     reference: __pet_ref_23
 247     read: 1
 248     write: 0
 249   - type: access
 250     relation: '[N] -> { S_9[t] -> __pet_test_3[-1 + t] : t >= 1 }'
 251     reference: __pet_ref_24
 252     read: 1
 253     write: 0
 254 - line: 29
 255   domain: '[N] -> { [S_10[t] -> [1, 0]] : t >= 0 }'
 256   schedule: '{ S_10[t] -> [3, t, 1, 1, 0] }'
 257   body:
 258     type: binary
 259     operation: =
 260     arguments:
 261     - type: access
 262       relation: '[N] -> { S_10[t] -> __pet_test_3[t] }'
 263       reference: __pet_ref_29
 264       read: 0
 265       write: 1
 266     - type: call
 267       name: f
 268   arguments:
 269   - type: access
 270     relation: '[N] -> { S_10[t] -> __pet_test_2[t] }'
 271     reference: __pet_ref_27
 272     read: 1
 273     write: 0
 274   - type: access
 275     relation: '[N] -> { S_10[t] -> __pet_test_3[-1 + t] : t >= 1 }'
 276     reference: __pet_ref_28
 277     read: 1
 278     write: 0
 279 - line: 31
 280   domain: '[N] -> { [S_11[t] -> [1, 0]] : t >= 0 }'
 281   schedule: '{ S_11[t] -> [3, t, 1, 2] }'
 282   body:
 283     type: binary
 284     operation: =
 285     arguments:
 286     - type: access
 287       relation: '[N] -> { S_11[t] -> a[] }'
 288       reference: __pet_ref_32
 289       read: 0
 290       write: 1
 291     - type: access
 292       relation: '[N] -> { S_11[t] -> [6] }'
 293       reference: __pet_ref_33
 294       read: 1
 295       write: 0
 296   arguments:
 297   - type: access
 298     relation: '[N] -> { S_11[t] -> __pet_test_2[t] }'
 299     reference: __pet_ref_30
 300     read: 1
 301     write: 0
 302   - type: access
 303     relation: '[N] -> { S_11[t] -> __pet_test_3[t] }'
 304     reference: __pet_ref_31
 305     read: 1
 306     write: 0
 307 implications:
 308 - satisfied: 0
 309   extension: '{ __pet_test_0[t] -> __pet_test_0[t''] : t'' <= t and t'' >= 0 }'
 310 - satisfied: 1
 311   extension: '[N] -> { __pet_test_1[t] -> __pet_test_1[t''] : N = 0 and t'' <= t and
 312     t'' >= 1; __pet_test_1[t] -> __pet_test_1[0] : t >= 0 }'
 313 - satisfied: 0
 314   extension: '{ __pet_test_3[t] -> __pet_test_3[t''] : t'' <= t and t'' >= 0 }'
 315 - satisfied: 1
 316   extension: '{ __pet_test_2[t] -> __pet_test_2[t''] : t'' <= t and t'' >= 0 }'