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

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabs_semantics.ma

    r2895 r2936  
    205205
    206206definition make_global : RTLabs_program → genv ≝
    207 λp. globalenv … (λx.[Init_space x]) p.
     207λp. globalenv … (λx.x) p.
    208208
    209209definition make_initial_state : RTLabs_program → res state ≝
    210210λp.
    211211  let ge ≝ make_global p in
    212   do m ← init_mem … (λx.[Init_space x]) p;
     212  do m ← init_mem … (λx.x) p;
    213213  let main ≝ prog_main ?? p in
    214214  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main);
Note: See TracChangeset for help on using the changeset viewer.