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