tests/while_break.scop

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