Ignore:
Timestamp:
Mar 21, 2013, 9:45:49 PM (6 years ago)
Author:
campbell
Message:

Disable initialisation code generation in Cminor, propogate init data
through RTLabs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/Cminor_semantics.ma

    r2722 r2936  
    430430  mk_fullexec … Cminor_exec make_global make_initial_state.
    431431
     432(* NB: we've pushed the initialisation code generation later, but here are the
     433   semantics for initialisation free Cminor anyway. *)   
     434
    432435definition make_noinit_global : Cminor_noinit_program → genv ≝
    433436λp. globalenv … (λx.[Init_space x]) p.
Note: See TracChangeset for help on using the changeset viewer.