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