Ignore:
Timestamp:
Jul 18, 2012, 1:26:43 PM (8 years ago)
Author:
tranquil
Message:
  • moving some code around
  • changed immediates to hold beval in general, not only bytes
  • fixed RTLabsToRTL after redefinitions in front end
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semanticsUtils_paolo.ma

    r2200 r2208  
    1414(*** Store/retrieve on hardware registers ***)
    1515
    16 definition init_hw_register_env: address → hw_register_env ≝
    17  λaddr.
    18   let 〈dpl,dph〉 ≝ addr in
     16definition init_hw_register_env: xpointer → hw_register_env ≝
     17 λsp.
     18  let 〈dpl,dph〉 ≝
     19    match beval_pair_of_pointer sp return λx.beval_pair_of_pointer sp = x → ? with
     20    [ OK p ⇒ λ_.p
     21    | _ ⇒ λprf.⊥
     22    ] (refl …) in
    1923  let env ≝ hwreg_store RegisterDPH dph empty_hw_register_env in
    2024   hwreg_store RegisterDPL dpl env.
     25@hide_prf
     26normalize in prf; destruct(prf)
     27qed.
    2128
    2229(******************************** GRAPHS **************************************)
Note: See TracChangeset for help on using the changeset viewer.