Ignore:
Timestamp:
Aug 30, 2011, 6:55:12 PM (8 years ago)
Author:
campbell
Message:

Merge trunk into branch.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/Cminor/semantics.ma

    r1135 r1153  
    466466definition make_initial_state : Cminor_program → res (genv × state) ≝
    467467λp.
    468   do ge ← globalenv Genv ?? p;
    469   do m ← init_mem Genv ?? p;
     468  do ge ← globalenv Genv ?? (λx.x) p;
     469  do m ← init_mem Genv ?? (λx.x) p;
    470470  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
    471471  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
     
    474474definition Cminor_fullexec : fullexec io_out io_in ≝
    475475  mk_fullexec … Cminor_exec ? make_initial_state.
     476
     477definition make_initial_noinit_state : Cminor_noinit_program → res (genv × state) ≝
     478λp.
     479  do ge ← globalenv Genv ?? (λx.[Init_space x]) p;
     480  do m ← init_mem Genv ?? (λx.[Init_space x]) p;
     481  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
     482  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
     483  OK ? 〈ge, Callstate f (nil ?) m SStop〉.
     484
     485definition Cminor_noinit_fullexec : fullexec io_out io_in ≝
     486  mk_fullexec … Cminor_exec ? make_initial_noinit_state.
Note: See TracChangeset for help on using the changeset viewer.