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