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/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.