Ignore:
Timestamp:
Aug 30, 2011, 12:47:18 PM (9 years ago)
Author:
campbell
Message:

Shift init_data out of generic program record so that it only appears
in programs that contain initialisation data (Clight and Cminor). Other
stages just have the size of each variable and translate it to Init_space
when building the initial state.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r1072 r1139  
    295295qed.
    296296
    297 definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
     297definition cminor_noinit_to_rtlabs : Cminor_noinit_program → res RTLabs_program ≝
    298298transform_partial_program ???
    299299  (transf_partial_fundef ?? c2ra_function).
     
    301301include "Cminor/initialisation.ma".
    302302
    303 definition cminor_init_to_rtlabs : Cminor_program → res RTLabs_program ≝
    304 λp. let p' ≝ replace_init p in cminor_to_rtlabs p.
     303definition cminor_to_rtlabs : Cminor_program → res RTLabs_program ≝
     304λp. let p' ≝ replace_init p in cminor_noinit_to_rtlabs p'.
Note: See TracChangeset for help on using the changeset viewer.