Ignore:
Timestamp:
Oct 19, 2011, 4:22:52 PM (9 years ago)
Author:
sacerdot
Message:
  1. hwreg_store/retrieve no longer returns a res (but it is still axiomatized)
  2. added initialization of local environment that sets the sp in the appropriate way
  3. ASM/I8051 splitted into ASM/I8051bis because of some bugs with disambiguation
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/SemanticUtils.ma

    r1408 r1415  
    1515axiom hw_register_env: Type[0]. (* CSC: use the one in I8051? *)
    1616axiom empty_hw_register_env: hw_register_env.
    17 axiom hwreg_retrieve : hw_register_env → Register → res beval.
    18 axiom hwreg_store : Register → beval → hw_register_env → res hw_register_env.
     17axiom hwreg_retrieve : hw_register_env → Register → beval.
     18axiom hwreg_store : Register → beval → hw_register_env → hw_register_env.
     19
     20definition init_hw_register_env: address → hw_register_env ≝
     21 λaddr.
     22  let 〈dpl,dph〉 ≝ addr in
     23  let env ≝ hwreg_store RegisterDPH dph empty_hw_register_env in
     24   hwreg_store RegisterDPL dpl env.
    1925
    2026(****************************************************************************)
Note: See TracChangeset for help on using the changeset viewer.