Changeset 1329 for src/joint/BEMem.ma


Ignore:
Timestamp:
Oct 7, 2011, 6:19:41 PM (9 years ago)
Author:
sacerdot
Message:
  1. Definition of addresses moved to BEMem
  2. Basic functions on addresses implemented in BEMem and used everywhere
  3. Semantics of ERTL extended statements completed
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/BEMem.ma

    r1213 r1329  
    1919axiom beloadv: ∀m:bemem. ∀ptr:pointer. option beval.
    2020axiom bestorev: ∀m:bemem. ∀ptr:pointer. beval → option bemem.
     21
     22(* CSC: only pointers to XRAM or code memory ATM *)
     23definition address ≝ beval × beval.
     24
     25definition eq_address: address → address → bool ≝
     26 λaddr1,addr2.
     27  eq_beval (\fst addr1) (\fst addr2) ∧ eq_beval (\snd addr1) (\snd addr2).
     28
     29definition pointer_of_address: address → res pointer ≝
     30 λp. let 〈v1,v2〉 ≝ p in pointer_of_bevals [v1;v2].
     31
     32(*CSC: for pointers of type Code and XData, the next function type can be
     33 strengthtened to never fail *)
     34definition address_of_pointer: pointer → res address ≝ beval_pair_of_pointer.
     35
     36definition addr_add: address → nat → res address ≝
     37 λaddr,n.
     38  do ptr ← pointer_of_address addr ;
     39  address_of_pointer (shift_pointer 16 ptr (bitvector_of_nat … n)).
     40
     41definition addr_sub: address → nat → res address ≝
     42 λaddr,n.
     43  do ptr ← pointer_of_address addr ;
     44  address_of_pointer (neg_shift_pointer 16 ptr (bitvector_of_nat … n)).
Note: See TracChangeset for help on using the changeset viewer.