Changeset 1408 for src/RTL/semantics.ma

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:

• src/RTL/semantics.ma (modified) (1 diff)

src/RTL/semantics.ma

@@ -14 +14 @@
 definition rtl_more_sem_params: more_sem_params rtl_params_ :=
  mk_more_sem_params rtl_params_
-  (list frame) (register_env beval) graph_succ_p
+  (list frame) [] (register_env beval) (empty_map …) [] [](*dummy*) graph_succ_p
    reg_store reg_retrieve reg_store reg_retrieve reg_store reg_retrieve
     reg_store reg_retrieve reg_store reg_retrieve