Changeset 1302 for src/joint


Ignore:
Timestamp:
Oct 5, 2011, 11:36:03 PM (9 years ago)
Author:
sacerdot
Message:

ERTL/semantics.ma ported to joint/SemanticUtils (in progress)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/SemanticUtils.ma

    r1300 r1302  
    11include "joint/semantics.ma".
    22
    3 (*** Store/retrieve on registers ***)
     3(*** Store/retrieve on pseudo-registers ***)
    44
    55axiom BadRegister : String.
     
    99definition reg_retrieve : register_env beval → register → res beval ≝
    1010 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).
     11
     12(*** Store/retrieve on hardware registers ***)
     13
     14axiom hw_register_env: Type[0]. (* CSC: use the one in I8051? *)
     15axiom hwreg_retrieve : hw_register_env → Register → res beval.
     16axiom hwreg_store : Register → beval → hw_register_env → res hw_register_env.
    1117
    1218(****************************************************************************)
Note: See TracChangeset for help on using the changeset viewer.