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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.