Ignore:
Timestamp:
Jul 13, 2012, 7:59:43 PM (8 years ago)
Author:
campbell
Message:

Use bitvectors for offsets.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Globalenvs.ma

    r2176 r2185  
    8282     addresses of the memory region in question - here there are no real
    8383     pointers, so use the real region. *)
    84   let ptr ≝ mk_pointer (*block_region m b*) b (*?*) (mk_offset p) in
     84  let ptr ≝ mk_pointer (*block_region m b*) b (*?*) (mk_offset (bitvector_of_Z … p)) in
    8585  match id with
    8686  [ Init_int8 n ⇒ store (ASTint I8 Unsigned) m ptr (Vint I8 n)
     
    236236| #f #fn #E normalize in E; destruct
    237237| (*#r*) #f #E normalize in E; destruct
    238 | * (*#pty*) #b (*#c*) * #off #f #E whd in E:(??%?);
    239   cases off in E ⊢ %; [ 2,3: #x ]
     238| * (*#pty*) #b (*#c*) * #off #f whd in ⊢ (??%? → ?);
     239  @eq_offset_elim #Eoff
    240240  #E whd in E:(??%?); destruct
    241241  (*%{pty}*) %{b} (*%{c}*) % // @E
Note: See TracChangeset for help on using the changeset viewer.