- Timestamp:
- Mar 21, 2013, 9:45:49 PM (7 years ago)
- Location:
- src
- Files:
-
- 5 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Cminor/Cminor_semantics.ma
r2722 r2936 430 430 mk_fullexec … Cminor_exec make_global make_initial_state. 431 431 432 (* NB: we've pushed the initialisation code generation later, but here are the 433 semantics for initialisation free Cminor anyway. *) 434 432 435 definition make_noinit_global : Cminor_noinit_program → genv ≝ 433 436 λp. globalenv … (λx.[Init_space x]) p. -
src/Cminor/toRTLabs.ma
r2924 r2936 939 939 qed. 940 940 941 definition cminor_ noinit_to_rtlabs : Cminor_noinit_program → RTLabs_program ≝941 definition cminor_to_rtlabs : Cminor_program → RTLabs_program ≝ 942 942 λp.transform_program … p (λ_. transf_fundef … c2ra_function). 943 943 944 include "Cminor/initialisation.ma".945 946 definition cminor_to_rtlabs : costlabel → Cminor_program → RTLabs_program ≝947 λinit_cost,p. let p' ≝ replace_init init_cost p in cminor_noinit_to_rtlabs p'. -
src/RTLabs/RTLabs_semantics.ma
r2895 r2936 205 205 206 206 definition make_global : RTLabs_program → genv ≝ 207 λp. globalenv … (λx. [Init_space x]) p.207 λp. globalenv … (λx.x) p. 208 208 209 209 definition make_initial_state : RTLabs_program → res state ≝ 210 210 λp. 211 211 let ge ≝ make_global p in 212 do m ← init_mem … (λx. [Init_space x]) p;212 do m ← init_mem … (λx.x) p; 213 213 let main ≝ prog_main ?? p in 214 214 do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main); -
src/RTLabs/RTLabs_syntax.ma
r2601 r2936 92 92 }. 93 93 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. 94 definition RTLabs_program ≝ program (λ_.fundef internal_function) (list init_data). 99 95 100 96 -
src/compiler.ma
r2907 r2936 70 70 ! p ← clight_to_cminor p; 71 71 let i ≝ observe cminor_pass p in 72 let p ≝ cminor_to_rtlabs init_costp in72 let p ≝ cminor_to_rtlabs p in 73 73 let i ≝ observe rtlabs_pass p in 74 74 if check_cost_program p then
Note: See TracChangeset
for help on using the changeset viewer.