Changeset 2936 for src/RTLabs


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

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

Location:
src/RTLabs
Files:
2 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);
  • src/RTLabs/RTLabs_syntax.ma

    r2601 r2936  
    9292}.
    9393
    94 (* Note that the global variables will be initialised by the code in main
    95    by this stage, so the only initialisation data is the amount of space to
    96    allocate. *)
    97 
    98 definition RTLabs_program ≝ program (λ_.fundef internal_function) nat.
     94definition RTLabs_program ≝ program (λ_.fundef internal_function) (list init_data).
    9995
    10096
Note: See TracChangeset for help on using the changeset viewer.