tests/while_break.scop

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