Changeset 1408 for src/RTLabs


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/RTLabs/RTLabsToRTL.ma

    r1358 r1408  
    439439  λdef: rtl_internal_function globals.
    440440  match op1 with
    441   [ Ocastint src_sign src_size
     441  [ Ocastint src_sign src_size _ _
    442442    let dest_size ≝ |destrs| * 8 in
    443443    let src_size ≝ bitsize_of_intsize src_size in
Note: See TracChangeset for help on using the changeset viewer.