tests/break6.scop

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