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