Ignore:
Timestamp:
Oct 19, 2011, 11:30:24 AM (8 years ago)
Author:
sacerdot
Message:
  1. Added joint/BEGlobalenvs that is a modification of common/Globalenvs where
    • the memory used is the back-end one
    • no lookup via values is implemented
    • global variables are never initialized in the back-end
  2. Added to all semantics some default value to initialize the initial state
  3. Initial state initialization (in joint/semantics.ma) almost completed.
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/SemanticUtils.ma

    r1395 r1408  
    1414
    1515axiom hw_register_env: Type[0]. (* CSC: use the one in I8051? *)
     16axiom empty_hw_register_env: hw_register_env.
    1617axiom hwreg_retrieve : hw_register_env → Register → res beval.
    1718axiom hwreg_store : Register → beval → hw_register_env → res hw_register_env.
Note: See TracChangeset for help on using the changeset viewer.