Ignore:
Timestamp:
Oct 6, 2011, 6:45:54 PM (9 years ago)
Author:
campbell
Message:

Merge trunk to invariants branch, sorting out the handling of temporaries
in Clight/toCminor.

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

    r1153 r1311  
    459459].
    460460
    461 definition Cminor_exec : execstep io_out io_in ≝
    462   mk_execstep … ? is_final mem_of_state eval_step.
     461definition Cminor_exec : trans_system io_out io_in ≝
     462  mk_trans_system … ? (λ_.is_final) eval_step.
    463463
    464464axiom MainMissing : String.
    465465
    466 definition make_initial_state : Cminor_program → res (genv × state) ≝
     466definition make_global : Cminor_program → genv ≝
     467λp. globalenv Genv ?? (λx.x) p.
     468
     469definition make_initial_state : Cminor_program → res state ≝
    467470λp.
    468   do ge ← globalenv Genv ?? (λx.x) p;
     471  let ge ≝ make_global p in
    469472  do m ← init_mem Genv ?? (λx.x) p;
    470473  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
    471474  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
    472   OK ? 〈ge, Callstate f (nil ?) m SStop〉.
     475  OK ? (Callstate f (nil ?) m SStop).
    473476
    474477definition Cminor_fullexec : fullexec io_out io_in ≝
    475   mk_fullexec … Cminor_exec ? make_initial_state.
    476 
    477 definition make_initial_noinit_state : Cminor_noinit_program → res (genv × state) ≝
     478  mk_fullexec … Cminor_exec make_global make_initial_state.
     479
     480definition make_noinit_global : Cminor_noinit_program → genv ≝
     481λp. globalenv Genv ?? (λx.[Init_space x]) p.
     482
     483definition make_initial_noinit_state : Cminor_noinit_program → res state ≝
    478484λp.
    479   do ge ← globalenv Genv ?? (λx.[Init_space x]) p;
     485  let ge ≝ make_noinit_global p in
    480486  do m ← init_mem Genv ?? (λx.[Init_space x]) p;
    481487  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
    482488  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
    483   OK ? 〈ge, Callstate f (nil ?) m SStop〉.
     489  OK ? (Callstate f (nil ?) m SStop).
    484490
    485491definition Cminor_noinit_fullexec : fullexec io_out io_in ≝
    486   mk_fullexec … Cminor_exec ? make_initial_noinit_state.
     492  mk_fullexec … Cminor_exec make_noinit_global make_initial_noinit_state.
Note: See TracChangeset for help on using the changeset viewer.