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/semantics.ma

    r961 r1139  
    274274definition make_initial_state : Cminor_program → res (genv × state) ≝
    275275λp.
    276   do ge ← globalenv Genv ?? p;
    277   do m ← init_mem Genv ?? p;
     276  do ge ← globalenv Genv ?? (λx.x) p;
     277  do m ← init_mem Genv ?? (λx.x) p;
    278278  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
    279279  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
     
    282282definition Cminor_fullexec : fullexec io_out io_in ≝
    283283  mk_fullexec … Cminor_exec ? make_initial_state.
     284
     285definition make_initial_noinit_state : Cminor_noinit_program → res (genv × state) ≝
     286λp.
     287  do ge ← globalenv Genv ?? (λx.[Init_space x]) p;
     288  do m ← init_mem Genv ?? (λx.[Init_space x]) p;
     289  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
     290  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
     291  OK ? 〈ge, Callstate f (nil ?) m Kstop〉.
     292
     293definition Cminor_noinit_fullexec : fullexec io_out io_in ≝
     294  mk_fullexec … Cminor_exec ? make_initial_noinit_state.
Note: See TracChangeset for help on using the changeset viewer.