Changeset 2185 for src/joint


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

Use bitvectors for offsets.

Location:
src/joint
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/joint/BEMem.ma

    r2176 r2185  
    118118*)
    119119lemma pointer_of_address_is_safe : ∀a : safe_address.pointer_of_address a = OK … (pointer_of_address_safe a).
    120 ** #a0 #a1 ***** #z #o 
     120** #a0 #a1 ***** #z #o
    121121#Hr
    122122(*
     
    127127destruct normalize
    128128@eqZb_elim [2,4,6: * #ABS elim (ABS (refl …))]
    129 @eqZb_elim [2,4,6: * #ABS elim (ABS (refl …))]
     129change with (eq_bv ???) in match (eq_v ?????);
     130@eq_bv_elim [2,4,6: * #ABS elim (ABS (refl …))]
    130131#_ #_ normalize %
    131132qed.
  • src/joint/semantics.ma

    r2176 r2185  
    228228      let l' ≝ joint_if_entry … fn in
    229229      let st ≝ set_regs p regs st in
    230       let pointer_in_fn ≝ mk_pointer (mk_block Code (block_id b)) (mk_offset 0) in
     230      let pointer_in_fn ≝ mk_pointer (mk_block Code (block_id b)) zero_offset in
    231231      ! newpc ← address_of_label … ge pointer_in_fn l' ;
    232232      let st ≝ set_pc … newpc st in
     
    401401 (* Invariant: a -1 block is unused in common/Globalenvs *)
    402402 let b ≝ mk_block Code (-1) in
    403  let ptr ≝ mk_pointer b (mk_offset 0) in
     403 let ptr ≝ mk_pointer b zero_offset in
    404404 let addr ≝ address_of_code_pointer ptr in
    405405  (λp. mk_evaluation_parameters (prog_var_names … p) (mk_sem_params2 … (sparams p)) addr (globalenv_noinit … p)).
     
    416416  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
    417417  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
    418   let dummy_pc ≝ mk_pointer (mk_block Code (-1)) (mk_offset 0) in
    419   let spp ≝ mk_pointer spb (mk_offset external_ram_size) in
    420   let ispp ≝ mk_pointer ispb (mk_offset 47) in
     418  let dummy_pc ≝ mk_pointer (mk_block Code (-1)) zero_offset in
     419  let spp ≝ mk_pointer spb (offset_of_Z external_ram_size) in
     420  let ispp ≝ mk_pointer ispb (offset_of_Z 47) in
    421421  do sp ← address_of_pointer spp ;
    422422  let main ≝ prog_main … p in
Note: See TracChangeset for help on using the changeset viewer.