Changeset 1408 for src/ERTL


Ignore:
Timestamp:
Oct 19, 2011, 11:30:24 AM (9 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/ERTL/semantics.ma

    r1390 r1408  
    2121definition ertl_more_sem_params: more_sem_params ertl_params_ :=
    2222 mk_more_sem_params ertl_params_
    23   (list (register_env beval)) ((register_env beval) × hw_register_env) graph_succ_p
     23  (list (register_env beval)) [] ((register_env beval) × hw_register_env)
     24   〈empty_map …,empty_hw_register_env〉 0 it
     25   graph_succ_p
    2426   ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
    2527    ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
Note: See TracChangeset for help on using the changeset viewer.