bench/encoding/why2/caduceus/trop_why.why

   1 logic eq_unit : unit, unit -> prop
   2
   3 logic neq_unit : unit, unit -> prop
   4
   5 logic eq_bool : bool, bool -> prop
   6
   7 logic neq_bool : bool, bool -> prop
   8
   9 logic lt_int : int, int -> prop
  10
  11 logic le_int : int, int -> prop
  12
  13 logic gt_int : int, int -> prop
  14
  15 logic ge_int : int, int -> prop
  16
  17 logic eq_int : int, int -> prop
  18
  19 logic neq_int : int, int -> prop
  20
  21 logic add_int : int, int -> int
  22
  23 logic sub_int : int, int -> int
  24
  25 logic mul_int : int, int -> int
  26
  27 logic div_int : int, int -> int
  28
  29 logic mod_int : int, int -> int
  30
  31 logic neg_int : int -> int
  32
  33 predicate zwf_zero(a: int, b: int) = ((0 <= b) and (a < b))
  34
  35 logic bw_compl : int -> int
  36
  37 logic bw_and : int, int -> int
  38
  39 logic bw_xor : int, int -> int
  40
  41 logic bw_or : int, int -> int
  42
  43 logic lsl : int, int -> int
  44
  45 logic lsr : int, int -> int
  46
  47 type 'z pointer
  48
  49 type 'z addr
  50
  51 type alloc_table
  52
  53 logic block_length : alloc_table, 'a1 pointer -> int
  54
  55 logic base_addr : 'a1 pointer -> 'a1 addr
  56
  57 logic offset : 'a1 pointer -> int
  58
  59 logic shift : 'a1 pointer, int -> 'a1 pointer
  60
  61 logic sub_pointer : 'a1 pointer, 'a1 pointer -> int
  62
  63 predicate lt_pointer(p1: 'a1 pointer, p2: 'a1 pointer) =
  64   ((base_addr(p1) = base_addr(p2)) and (offset(p1) < offset(p2)))
  65
  66 predicate le_pointer(p1: 'a1 pointer, p2: 'a1 pointer) =
  67   ((base_addr(p1) = base_addr(p2)) and (offset(p1) <= offset(p2)))
  68
  69 predicate gt_pointer(p1: 'a1 pointer, p2: 'a1 pointer) =
  70   ((base_addr(p1) = base_addr(p2)) and (offset(p1) > offset(p2)))
  71
  72 predicate ge_pointer(p1: 'a1 pointer, p2: 'a1 pointer) =
  73   ((base_addr(p1) = base_addr(p2)) and (offset(p1) >= offset(p2)))
  74
  75 predicate valid(a: alloc_table, p: 'a1 pointer) =
  76   ((0 <= offset(p)) and (offset(p) < block_length(a, p)))
  77
  78 predicate valid_index(a: alloc_table, p: 'a1 pointer, i: int) =
  79   ((0 <= (offset(p) + i)) and ((offset(p) + i) < block_length(a, p)))
  80
  81 predicate valid_range(a: alloc_table, p: 'a1 pointer, i: int, j: int) =
  82   ((0 <= (offset(p) + i)) and ((offset(p) + j) < block_length(a, p)))
  83
  84 axiom offset_shift:
  85   (forall p:'a1 pointer.
  86     (forall i:int [offset(shift(p, i))]. (offset(shift(p,
  87       i)) = (offset(p) + i))))
  88
  89 axiom shift_zero: (forall p:'a1 pointer [shift(p, 0)]. (shift(p, 0) = p))
  90
  91 axiom shift_shift:
  92   (forall p:'a1 pointer.
  93     (forall i:int.
  94       (forall j:int [shift(shift(p, i), j)]. (shift(shift(p, i),
  95         j) = shift(p, (i + j))))))
  96
  97 axiom base_addr_shift:
  98   (forall p:'a1 pointer.
  99     (forall i:int [base_addr(shift(p, i))]. (base_addr(shift(p,
 100       i)) = base_addr(p))))
 101
 102 axiom block_length_shift:
 103   (forall a:alloc_table.
 104     (forall p:'a1 pointer.
 105       (forall i:int [block_length(a, shift(p, i))]. (block_length(a, shift(p,
 106         i)) = block_length(a, p)))))
 107
 108 axiom base_addr_block_length:
 109   (forall a:alloc_table.
 110     (forall p1:'a1 pointer.
 111       (forall p2:'a1 pointer.
 112         ((base_addr(p1) = base_addr(p2)) -> (block_length(a,
 113          p1) = block_length(a, p2))))))
 114
 115 axiom pointer_pair_1:
 116   (forall p1:'a1 pointer.
 117     (forall p2:'a1 pointer.
 118       (((base_addr(p1) = base_addr(p2)) and (offset(p1) = offset(p2))) ->
 119        (p1 = p2))))
 120
 121 axiom pointer_pair_2:
 122   (forall p1:'a1 pointer.
 123     (forall p2:'a1 pointer.
 124       ((p1 = p2) ->
 125        ((base_addr(p1) = base_addr(p2)) and (offset(p1) = offset(p2))))))
 126
 127 axiom neq_base_addr_neq_shift:
 128   (forall p1:'a1 pointer.
 129     (forall p2:'a1 pointer.
 130       (forall i:int.
 131         (forall j:int.
 132           ((base_addr(p1) <> base_addr(p2)) -> (shift(p1, i) <> shift(p2, j)))))))
 133
 134 axiom neq_offset_neq_shift:
 135   (forall p1:'a1 pointer.
 136     (forall p2:'a1 pointer.
 137       (forall i:int.
 138         (forall j:int.
 139           (((offset(p1) + i) <> (offset(p2) + j)) -> (shift(p1,
 140            i) <> shift(p2, j)))))))
 141
 142 axiom eq_offset_eq_shift:
 143   (forall p1:'a1 pointer.
 144     (forall p2:'a1 pointer.
 145       (forall i:int.
 146         (forall j:int.
 147           ((base_addr(p1) = base_addr(p2)) ->
 148            (((offset(p1) + i) = (offset(p2) + j)) -> (shift(p1,
 149             i) = shift(p2, j))))))))
 150
 151 axiom valid_index_valid_shift:
 152   (forall a:alloc_table.
 153     (forall p:'a1 pointer.
 154       (forall i:int. (valid_index(a, p, i) -> valid(a, shift(p, i))))))
 155
 156 axiom valid_range_valid_shift:
 157   (forall a:alloc_table.
 158     (forall p:'a1 pointer.
 159       (forall i:int.
 160         (forall j:int.
 161           (forall k:int.
 162             (valid_range(a, p, i, j) ->
 163              (((i <= k) and (k <= j)) -> valid(a, shift(p, k)))))))))
 164
 165 axiom valid_range_valid:
 166   (forall a:alloc_table.
 167     (forall p:'a1 pointer.
 168       (forall i:int.
 169         (forall j:int.
 170           (valid_range(a, p, i, j) ->
 171            (((i <= 0) and (0 <= j)) -> valid(a, p)))))))
 172
 173 axiom valid_range_valid_index:
 174   (forall a:alloc_table.
 175     (forall p:'a1 pointer.
 176       (forall i:int.
 177         (forall j:int.
 178           (forall k:int.
 179             (valid_range(a, p, i, j) ->
 180              (((i <= k) and (k <= j)) -> valid_index(a, p, k))))))))
 181
 182 axiom sub_pointer_def:
 183   (forall p1:'a1 pointer.
 184     (forall p2:'a1 pointer.
 185       ((base_addr(p1) = base_addr(p2)) -> (sub_pointer(p1,
 186        p2) = (offset(p1) - offset(p2))))))
 187
 188 type ('a, 'z) memory
 189
 190 logic acc : ('a1, 'a2) memory, 'a2 pointer -> 'a1
 191
 192 logic upd : ('a1, 'a2) memory, 'a2 pointer, 'a1 -> ('a1, 'a2) memory
 193
 194 axiom acc_upd:
 195   (forall m:('a1, 'a2) memory.
 196     (forall p:'a2 pointer.
 197       (forall a:'a1 [acc(upd(m, p, a), p)]. (acc(upd(m, p, a), p) = a))))
 198
 199 axiom acc_upd_neq:
 200   (forall m:('a1, 'a2) memory.
 201     (forall p1:'a2 pointer.
 202       (forall p2:'a2 pointer.
 203         (forall a:'a1 [acc(upd(m, p1, a), p2)].
 204           ((p1 <> p2) -> (acc(upd(m, p1, a), p2) = acc(m, p2)))))))
 205
 206 axiom false_not_true: (false <> true)
 207
 208 type 'z pset
 209
 210 logic pset_empty : 'a1 pset
 211
 212 logic pset_singleton : 'a1 pointer -> 'a1 pset
 213
 214 logic pset_star : 'a2 pset, ('a1 pointer, 'a2) memory -> 'a1 pset
 215
 216 logic pset_all : 'a1 pset -> 'a1 pset
 217
 218 logic pset_range : 'a1 pset, int, int -> 'a1 pset
 219
 220 logic pset_range_left : 'a1 pset, int -> 'a1 pset
 221
 222 logic pset_range_right : 'a1 pset, int -> 'a1 pset
 223
 224 logic pset_acc_all : 'a2 pset, ('a1 pointer, 'a2) memory -> 'a1 pset
 225
 226 logic pset_acc_range : 'a2 pset, ('a1 pointer, 'a2) memory, int,
 227 int -> 'a1 pset
 228
 229 logic pset_acc_range_left : 'a2 pset, ('a1 pointer, 'a2) memory,
 230 int -> 'a1 pset
 231
 232 logic pset_acc_range_right : 'a2 pset, ('a1 pointer, 'a2) memory,
 233 int -> 'a1 pset
 234
 235 logic pset_union : 'a1 pset, 'a1 pset -> 'a1 pset
 236
 237 logic not_in_pset : 'a1 pointer, 'a1 pset -> prop
 238
 239 predicate not_assigns(a: alloc_table, m1: ('a1, 'a2) memory, m2: ('a1,
 240   'a2) memory, l: 'a2 pset) =
 241   (forall p:'a2 pointer.
 242     (valid(a, p) -> (not_in_pset(p, l) -> (acc(m2, p) = acc(m1, p)))))
 243
 244 axiom pset_empty_intro: (forall p:'a1 pointer. not_in_pset(p, pset_empty))
 245
 246 axiom pset_singleton_intro:
 247   (forall p1:'a1 pointer.
 248     (forall p2:'a1 pointer [not_in_pset(p1, pset_singleton(p2))].
 249       ((p1 <> p2) -> not_in_pset(p1, pset_singleton(p2)))))
 250
 251 axiom pset_singleton_elim:
 252   (forall p1:'a1 pointer.
 253     (forall p2:'a1 pointer [not_in_pset(p1, pset_singleton(p2))].
 254       (not_in_pset(p1, pset_singleton(p2)) -> (p1 <> p2))))
 255
 256 axiom not_not_in_singleton:
 257   (forall p:'a1 pointer. (not not_in_pset(p, pset_singleton(p))))
 258
 259 axiom pset_union_intro:
 260   (forall l1:'a1 pset.
 261     (forall l2:'a1 pset.
 262       (forall p:'a1 pointer [not_in_pset(p, pset_union(l1, l2))].
 263         ((not_in_pset(p, l1) and not_in_pset(p, l2)) -> not_in_pset(p,
 264          pset_union(l1, l2))))))
 265
 266 axiom pset_union_elim1:
 267   (forall l1:'a1 pset.
 268     (forall l2:'a1 pset.
 269       (forall p:'a1 pointer [not_in_pset(p, pset_union(l1, l2))].
 270         (not_in_pset(p, pset_union(l1, l2)) -> not_in_pset(p, l1)))))
 271
 272 axiom pset_union_elim2:
 273   (forall l1:'a1 pset.
 274     (forall l2:'a1 pset.
 275       (forall p:'a1 pointer [not_in_pset(p, pset_union(l1, l2))].
 276         (not_in_pset(p, pset_union(l1, l2)) -> not_in_pset(p, l2)))))
 277
 278 axiom pset_star_intro:
 279   (forall l:'a1 pset.
 280     (forall m:('a2 pointer, 'a1) memory.
 281       (forall p:'a2 pointer [not_in_pset(p, pset_star(l, m))].
 282         ((forall p1:'a1 pointer. ((p = acc(m, p1)) -> not_in_pset(p1, l))) ->
 283          not_in_pset(p, pset_star(l, m))))))
 284
 285 axiom pset_star_elim:
 286   (forall l:'a1 pset.
 287     (forall m:('a2 pointer, 'a1) memory.
 288       (forall p:'a2 pointer [not_in_pset(p, pset_star(l, m))].
 289         (not_in_pset(p, pset_star(l, m)) ->
 290          (forall p1:'a1 pointer. ((p = acc(m, p1)) -> not_in_pset(p1, l)))))))
 291
 292 axiom pset_all_intro:
 293   (forall p:'a1 pointer.
 294     (forall l:'a1 pset [not_in_pset(p, pset_all(l))].
 295       ((forall p1:'a1 pointer.
 296          ((not not_in_pset(p1, l)) -> (base_addr(p) <> base_addr(p1)))) ->
 297        not_in_pset(p, pset_all(l)))))
 298
 299 axiom pset_all_elim:
 300   (forall p:'a1 pointer.
 301     (forall l:'a1 pset [not_in_pset(p, pset_all(l))].
 302       (not_in_pset(p, pset_all(l)) ->
 303        (forall p1:'a1 pointer.
 304          ((not not_in_pset(p1, l)) -> (base_addr(p) <> base_addr(p1)))))))
 305
 306 axiom pset_range_intro:
 307   (forall p:'a1 pointer.
 308     (forall l:'a1 pset.
 309       (forall a:int.
 310         (forall b:int [not_in_pset(p, pset_range(l, a, b))].
 311           ((forall p1:'a1 pointer.
 312              (not_in_pset(p1, l) or
 313               (forall i:int.
 314                 (((a <= i) and (i <= b)) -> (p <> shift(p1, i)))))) ->
 315            not_in_pset(p, pset_range(l, a, b)))))))
 316
 317 axiom pset_range_elim:
 318   (forall p:'a1 pointer.
 319     (forall l:'a1 pset.
 320       (forall a:int.
 321         (forall b:int [not_in_pset(p, pset_range(l, a, b))].
 322           (not_in_pset(p, pset_range(l, a, b)) ->
 323            (forall p1:'a1 pointer.
 324              ((not not_in_pset(p1, l)) ->
 325               (forall i:int.
 326                 (((a <= i) and (i <= b)) -> (shift(p1, i) <> p))))))))))
 327
 328 axiom pset_range_left_intro:
 329   (forall p:'a1 pointer.
 330     (forall l:'a1 pset.
 331       (forall a:int [not_in_pset(p, pset_range_left(l, a))].
 332         ((forall p1:'a1 pointer.
 333            (not_in_pset(p1, l) or
 334             (forall i:int. ((i <= a) -> (p <> shift(p1, i)))))) ->
 335          not_in_pset(p, pset_range_left(l, a))))))
 336
 337 axiom pset_range_left_elim:
 338   (forall p:'a1 pointer.
 339     (forall l:'a1 pset.
 340       (forall a:int [not_in_pset(p, pset_range_left(l, a))].
 341         (not_in_pset(p, pset_range_left(l, a)) ->
 342          (forall p1:'a1 pointer.
 343            ((not not_in_pset(p1, l)) ->
 344             (forall i:int. ((i <= a) -> (shift(p1, i) <> p)))))))))
 345
 346 axiom pset_range_right_intro:
 347   (forall p:'a1 pointer.
 348     (forall l:'a1 pset.
 349       (forall a:int [not_in_pset(p, pset_range_right(l, a))].
 350         ((forall p1:'a1 pointer.
 351            (not_in_pset(p1, l) or
 352             (forall i:int. ((a <= i) -> (p <> shift(p1, i)))))) ->
 353          not_in_pset(p, pset_range_right(l, a))))))
 354
 355 axiom pset_range_right_elim:
 356   (forall p:'a1 pointer.
 357     (forall l:'a1 pset.
 358       (forall a:int [not_in_pset(p, pset_range_right(l, a))].
 359         (not_in_pset(p, pset_range_right(l, a)) ->
 360          (forall p1:'a1 pointer.
 361            ((not not_in_pset(p1, l)) ->
 362             (forall i:int. ((a <= i) -> (shift(p1, i) <> p)))))))))
 363
 364 axiom pset_acc_all_intro:
 365   (forall p:'a1 pointer.
 366     (forall l:'a2 pset.
 367       (forall m:('a1 pointer, 'a2) memory [not_in_pset(p, pset_acc_all(l,
 368         m))].
 369         ((forall p1:'a2 pointer.
 370            ((not not_in_pset(p1, l)) ->
 371             (forall i:int. (p <> acc(m, shift(p1, i)))))) ->
 372          not_in_pset(p, pset_acc_all(l, m))))))
 373
 374 axiom pset_acc_all_elim:
 375   (forall p:'a1 pointer.
 376     (forall l:'a2 pset.
 377       (forall m:('a1 pointer, 'a2) memory [not_in_pset(p, pset_acc_all(l,
 378         m))].
 379         (not_in_pset(p, pset_acc_all(l, m)) ->
 380          (forall p1:'a2 pointer.
 381            ((not not_in_pset(p1, l)) ->
 382             (forall i:int. (acc(m, shift(p1, i)) <> p))))))))
 383
 384 axiom pset_acc_range_intro:
 385   (forall p:'a1 pointer.
 386     (forall l:'a2 pset.
 387       (forall m:('a1 pointer, 'a2) memory.
 388         (forall a:int.
 389           (forall b:int [not_in_pset(p, pset_acc_range(l, m, a, b))].
 390             ((forall p1:'a2 pointer.
 391                ((not not_in_pset(p1, l)) ->
 392                 (forall i:int.
 393                   (((a <= i) and (i <= b)) -> (p <> acc(m, shift(p1, i))))))) ->
 394              not_in_pset(p, pset_acc_range(l, m, a, b))))))))
 395
 396 axiom pset_acc_range_elim:
 397   (forall p:'a1 pointer.
 398     (forall l:'a2 pset.
 399       (forall m:('a1 pointer, 'a2) memory.
 400         (forall a:int.
 401           (forall b:int.
 402             (not_in_pset(p, pset_acc_range(l, m, a, b)) ->
 403              (forall p1:'a2 pointer.
 404                ((not not_in_pset(p1, l)) ->
 405                 (forall i:int.
 406                   (((a <= i) and (i <= b)) -> (acc(m, shift(p1, i)) <> p)))))))))))
 407
 408 axiom pset_acc_range_left_intro:
 409   (forall p:'a1 pointer.
 410     (forall l:'a2 pset.
 411       (forall m:('a1 pointer, 'a2) memory.
 412         (forall a:int [not_in_pset(p, pset_acc_range_left(l, m, a))].
 413           ((forall p1:'a2 pointer.
 414              ((not not_in_pset(p1, l)) ->
 415               (forall i:int. ((i <= a) -> (p <> acc(m, shift(p1, i))))))) ->
 416            not_in_pset(p, pset_acc_range_left(l, m, a)))))))
 417
 418 axiom pset_acc_range_left_elim:
 419   (forall p:'a1 pointer.
 420     (forall l:'a2 pset.
 421       (forall m:('a1 pointer, 'a2) memory.
 422         (forall a:int [not_in_pset(p, pset_acc_range_left(l, m, a))].
 423           (not_in_pset(p, pset_acc_range_left(l, m, a)) ->
 424            (forall p1:'a2 pointer.
 425              ((not not_in_pset(p1, l)) ->
 426               (forall i:int. ((i <= a) -> (acc(m, shift(p1, i)) <> p))))))))))
 427
 428 axiom pset_acc_range_right_intro:
 429   (forall p:'a1 pointer.
 430     (forall l:'a2 pset.
 431       (forall m:('a1 pointer, 'a2) memory.
 432         (forall a:int [not_in_pset(p, pset_acc_range_right(l, m, a))].
 433           ((forall p1:'a2 pointer.
 434              ((not not_in_pset(p1, l)) ->
 435               (forall i:int. ((a <= i) -> (p <> acc(m, shift(p1, i))))))) ->
 436            not_in_pset(p, pset_acc_range_right(l, m, a)))))))
 437
 438 axiom pset_acc_range_right_elim:
 439   (forall p:'a1 pointer.
 440     (forall l:'a2 pset.
 441       (forall m:('a1 pointer, 'a2) memory.
 442         (forall a:int [not_in_pset(p, pset_acc_range_right(l, m, a))].
 443           (not_in_pset(p, pset_acc_range_right(l, m, a)) ->
 444            (forall p1:'a2 pointer.
 445              ((not not_in_pset(p1, l)) ->
 446               (forall i:int. ((a <= i) -> (acc(m, shift(p1, i)) <> p))))))))))
 447
 448 axiom not_assigns_trans:
 449   (forall a:alloc_table.
 450     (forall l:'a1 pset.
 451       (forall m1:('a2, 'a1) memory.
 452         (forall m2:('a2, 'a1) memory.
 453           (forall m3:('a2, 'a1) memory.
 454             (not_assigns(a, m1, m2, l) ->
 455              (not_assigns(a, m2, m3, l) -> not_assigns(a, m1, m3, l))))))))
 456
 457 axiom not_assigns_refl:
 458   (forall a:alloc_table.
 459     (forall l:'a1 pset.
 460       (forall m:('a2, 'a1) memory. not_assigns(a, m, m, l))))
 461
 462 predicate valid_acc(m1: ('a1 pointer, 'a2) memory) =
 463   (forall p:'a2 pointer.
 464     (forall a:alloc_table. (valid(a, p) -> valid(a, acc(m1, p)))))
 465
 466 predicate valid_acc_range(m1: ('a1 pointer, 'a2) memory, size: int) =
 467   (forall p:'a2 pointer.
 468     (forall a:alloc_table.
 469       (valid(a, p) -> valid_range(a, acc(m1, p), 0, (size - 1)))))
 470
 471 axiom valid_acc_range_valid:
 472   (forall m1:('a1 pointer, 'a2) memory.
 473     (forall size:int.
 474       (forall p:'a2 pointer.
 475         (forall a:alloc_table.
 476           (valid_acc_range(m1, size) -> (valid(a, p) -> valid(a, acc(m1, p))))))))
 477
 478 predicate separation1(m1: ('a1 pointer, 'a2) memory, m2: ('a1 pointer,
 479   'a2) memory) =
 480   (forall p:'a2 pointer.
 481     (forall a:alloc_table.
 482       (valid(a, p) -> (base_addr(acc(m1, p)) <> base_addr(acc(m2, p))))))
 483
 484 predicate separation1_range1(m1: ('a1 pointer, 'a2) memory, m2: ('a1 pointer,
 485   'a2) memory, size: int) =
 486   (forall p:'a2 pointer.
 487     (forall a:alloc_table.
 488       (valid(a, p) ->
 489        (forall i1:int.
 490          (forall i2:int.
 491            (((0 <= i1) and (i1 < size)) ->
 492             (((0 <= i2) and (i2 < size)) -> (base_addr(acc(m1, shift(p,
 493              i1))) <> base_addr(acc(m2, shift(p, i2)))))))))))
 494
 495 predicate separation1_range(m: ('a1 pointer, 'a2) memory, size: int) =
 496   (forall p:'a2 pointer.
 497     (forall a:alloc_table.
 498       (valid(a, p) ->
 499        (forall i1:int.
 500          (((0 <= i1) and (i1 < size)) -> (base_addr(acc(m, shift(p,
 501           i1))) <> base_addr(acc(m, p))))))))
 502
 503 predicate separation2(m1: ('a1 pointer, 'a2) memory, m2: ('a1 pointer,
 504   'a2) memory) =
 505   (forall p1:'a2 pointer.
 506     (forall p2:'a2 pointer.
 507       ((p1 <> p2) -> (base_addr(acc(m1, p1)) <> base_addr(acc(m2, p2))))))
 508
 509 predicate separation2_range1(m1: ('a1 pointer, 'a2) memory, m2: ('a1 pointer,
 510   'a2) memory, size: int) =
 511   (forall p:'a2 pointer.
 512     (forall q:'a2 pointer.
 513       (forall a:alloc_table.
 514         (forall i:int.
 515           (((0 <= i) and (i < size)) -> (base_addr(acc(m1, shift(p,
 516            i))) <> base_addr(acc(m2, q))))))))
 517
 518 logic on_heap : alloc_table, 'a1 pointer -> prop
 519
 520 logic on_stack : alloc_table, 'a1 pointer -> prop
 521
 522 logic fresh : alloc_table, 'a1 pointer -> prop
 523
 524 axiom fresh_not_valid:
 525   (forall a:alloc_table.
 526     (forall p:'a1 pointer. (fresh(a, p) -> (not valid(a, p)))))
 527
 528 axiom fresh_not_valid_shift:
 529   (forall a:alloc_table.
 530     (forall p:'a1 pointer.
 531       (fresh(a, p) -> (forall i:int. (not valid(a, shift(p, i)))))))
 532
 533 logic alloc_extends : alloc_table, alloc_table -> prop
 534
 535 axiom alloc_extends_valid:
 536   (forall a1:alloc_table.
 537     (forall a2:alloc_table.
 538       (alloc_extends(a1, a2) ->
 539        (forall q:'a1 pointer. (valid(a1, q) -> valid(a2, q))))))
 540
 541 axiom alloc_extends_valid_index:
 542   (forall a1:alloc_table.
 543     (forall a2:alloc_table.
 544       (alloc_extends(a1, a2) ->
 545        (forall q:'a1 pointer.
 546          (forall i:int. (valid_index(a1, q, i) -> valid_index(a2, q, i)))))))
 547
 548 axiom alloc_extends_valid_range:
 549   (forall a1:alloc_table.
 550     (forall a2:alloc_table.
 551       (alloc_extends(a1, a2) ->
 552        (forall q:'a1 pointer.
 553          (forall i:int.
 554            (forall j:int.
 555              (valid_range(a1, q, i, j) -> valid_range(a2, q, i, j))))))))
 556
 557 axiom alloc_extends_refl: (forall a:alloc_table. alloc_extends(a, a))
 558
 559 axiom alloc_extends_trans:
 560   (forall a1:alloc_table.
 561     (forall a2:alloc_table.
 562       (forall a3:alloc_table [alloc_extends(a1, a2), alloc_extends(a2, a3)].
 563         (alloc_extends(a1, a2) ->
 564          (alloc_extends(a2, a3) -> alloc_extends(a1, a3))))))
 565
 566 logic free_stack : alloc_table, alloc_table, alloc_table -> prop
 567
 568 axiom free_stack_heap:
 569   (forall a1:alloc_table.
 570     (forall a2:alloc_table.
 571       (forall a3:alloc_table.
 572         (free_stack(a1, a2, a3) ->
 573          (forall p:'a1 pointer.
 574            (valid(a2, p) -> (on_heap(a2, p) -> valid(a3, p))))))))
 575
 576 axiom free_stack_stack:
 577   (forall a1:alloc_table.
 578     (forall a2:alloc_table.
 579       (forall a3:alloc_table.
 580         (free_stack(a1, a2, a3) ->
 581          (forall p:'a1 pointer.
 582            (valid(a1, p) -> (on_stack(a1, p) -> valid(a3, p))))))))
 583
 584 logic null : 'a1 pointer
 585
 586 axiom null_not_valid: (forall a:alloc_table. (not valid(a, null)))
 587
 588 type v_4
 589
 590 type index_1_17
 591
 592 type v_5
 593
 594 type ta_1_12
 595
 596 type lasPM_20
 597
 598 type ta_1_18
 599
 600 type lasPM_23
 601
 602 type ta_1_19
 603
 604 type lasPM_25
 605
 606 type ta_1_22
 607
 608 type null_6
 609
 610 type u_2
 611
 612 type null_7
 613
 614 type u_3
 615
 616 type index_0_16
 617
 618 type v_10
 619
 620 type ta_1_26
 621
 622 type v_11
 623
 624 type u_8
 625
 626 type u_9
 627
 628 type ta_1
 629
 630 type lasPM_20_21
 631
 632 type lasPM_20_24
 633
 634 type p_0
 635
 636 goal f_impl_po_1:
 637   forall alloc:alloc_table.
 638   forall p_u_9:(null_6 pointer, u_9) memory.
 639   forall ta_u_9:(null_6 pointer,
 640   u_9) memory.
 641   forall u:u_9 pointer.
 642   (("CADUCEUS_1":
 643    (valid(alloc, acc(p_u_9, u)) and (base_addr(acc(ta_u_9,
 644     u)) <> base_addr(acc(p_u_9, u))))) and
 645    (("CADUCEUS_4": valid(alloc, u)) and
 646     (("CADUCEUS_3": valid_acc_range(ta_u_9, 1)) and
 647      ("CADUCEUS_2": valid_acc(ta_u_9))))) ->
 648   valid(alloc, u)
 649
 650 goal f_impl_po_2:
 651   forall alloc:alloc_table.
 652   forall intM_null_6:(int, null_6) memory.
 653   forall p_u_9:(null_6 pointer, u_9) memory.
 654   forall ta_u_9:(null_6 pointer,
 655   u_9) memory.
 656   forall u:u_9 pointer.
 657   (("CADUCEUS_1":
 658    (valid(alloc, acc(p_u_9, u)) and (base_addr(acc(ta_u_9,
 659     u)) <> base_addr(acc(p_u_9, u))))) and
 660    (("CADUCEUS_4": valid(alloc, u)) and
 661     (("CADUCEUS_3": valid_acc_range(ta_u_9, 1)) and
 662      ("CADUCEUS_2": valid_acc(ta_u_9))))) ->
 663   valid(alloc, u) ->
 664   forall result:null_6 pointer.
 665   (result = acc(ta_u_9, u)) ->
 666   forall result0:null_6 pointer.
 667   (result0 = shift(result, 0)) ->
 668   forall intM_null_6_0:(int,
 669   null_6) memory.
 670   (intM_null_6_0 = upd(intM_null_6, result0, 0)) ->
 671   valid(alloc, u) ->
 672   forall result1:null_6 pointer.
 673   (result1 = acc(p_u_9, u)) ->
 674   valid(alloc, result1)
 675
 676 goal f_impl_po_3:
 677   forall alloc:alloc_table.
 678   forall intM_null_6:(int, null_6) memory.
 679   forall p_u_9:(null_6 pointer, u_9) memory.
 680   forall ta_u_9:(null_6 pointer,
 681   u_9) memory.
 682   forall u:u_9 pointer.
 683   (("CADUCEUS_1":
 684    (valid(alloc, acc(p_u_9, u)) and (base_addr(acc(ta_u_9,
 685     u)) <> base_addr(acc(p_u_9, u))))) and
 686    (("CADUCEUS_4": valid(alloc, u)) and
 687     (("CADUCEUS_3": valid_acc_range(ta_u_9, 1)) and
 688      ("CADUCEUS_2": valid_acc(ta_u_9))))) ->
 689   valid(alloc, u) ->
 690   forall result:null_6 pointer.
 691   (result = acc(ta_u_9, u)) ->
 692   forall result0:null_6 pointer.
 693   (result0 = shift(result, 0)) ->
 694   forall intM_null_6_0:(int,
 695   null_6) memory.
 696   (intM_null_6_0 = upd(intM_null_6, result0, 0)) ->
 697   valid(alloc, u) ->
 698   forall result1:null_6 pointer.
 699   (result1 = acc(p_u_9, u)) ->
 700   valid(alloc, result1) ->
 701   forall intM_null_6_1:(int,
 702   null_6) memory.
 703   (intM_null_6_1 = upd(intM_null_6_0, result1, 5)) ->
 704   ("CADUCEUS_6": ("CADUCEUS_6": (acc(intM_null_6_1, acc(ta_u_9, u)) = 0)))
 705
 706 goal f_impl_po_4:
 707   forall alloc:alloc_table.
 708   forall intM_null_6:(int, null_6) memory.
 709   forall p_u_9:(null_6 pointer, u_9) memory.
 710   forall ta_u_9:(null_6 pointer,
 711   u_9) memory.
 712   forall u:u_9 pointer.
 713   (("CADUCEUS_1":
 714    (valid(alloc, acc(p_u_9, u)) and (base_addr(acc(ta_u_9,
 715     u)) <> base_addr(acc(p_u_9, u))))) and
 716    (("CADUCEUS_4": valid(alloc, u)) and
 717     (("CADUCEUS_3": valid_acc_range(ta_u_9, 1)) and
 718      ("CADUCEUS_2": valid_acc(ta_u_9))))) ->
 719   valid(alloc, u) ->
 720   forall result:null_6 pointer.
 721   (result = acc(ta_u_9, u)) ->
 722   forall result0:null_6 pointer.
 723   (result0 = shift(result, 0)) ->
 724   forall intM_null_6_0:(int,
 725   null_6) memory.
 726   (intM_null_6_0 = upd(intM_null_6, result0, 0)) ->
 727   valid(alloc, u) ->
 728   forall result1:null_6 pointer.
 729   (result1 = acc(p_u_9, u)) ->
 730   valid(alloc, result1) ->
 731   forall intM_null_6_1:(int,
 732   null_6) memory.
 733   (intM_null_6_1 = upd(intM_null_6_0, result1, 5)) ->
 734   ("CADUCEUS_5":
 735   ("CADUCEUS_5": not_assigns(alloc, intM_null_6, intM_null_6_1,
 736   pset_union(pset_singleton(acc(ta_u_9, u)), pset_singleton(acc(p_u_9, u))))))
 737