Changeset 1408 for src/RTLabs

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/RTLabs/RTLabsToRTL.ma (modified) (1 diff)

src/RTLabs/RTLabsToRTL.ma

@@ -439 +439 @@
   λdef: rtl_internal_function globals.
   match op1 with
-  [ Ocastint src_sign src_size ⇒
+  [ Ocastint src_sign src_size _ _ ⇒
     let dest_size ≝ |destrs| * 8 in
     let src_size ≝ bitsize_of_intsize src_size in