Ignore:
Timestamp:
Sep 21, 2011, 4:25:36 PM (8 years ago)
Author:
campbell
Message:

Update Cminor and RTLabs to fit SmallstepExec? changes.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/semantics.ma

    r1139 r1238  
    267267].
    268268
    269 definition Cminor_exec : execstep io_out io_in ≝
    270   mk_execstep … ? is_final mem_of_state eval_step.
     269definition Cminor_exec : trans_system io_out io_in ≝
     270  mk_trans_system … ? (λ_.is_final) eval_step.
    271271
    272272axiom MainMissing : String.
    273273
    274 definition make_initial_state : Cminor_program → res (genv × state) ≝
     274definition make_global : Cminor_program → genv ≝
     275λp. globalenv Genv ?? (λx.x) p.
     276
     277definition make_initial_state : Cminor_program → res state ≝
    275278λp.
    276   do ge ← globalenv Genv ?? (λx.x) p;
     279  let ge ≝ make_global p in
    277280  do m ← init_mem Genv ?? (λx.x) p;
    278281  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
    279282  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
    280   OK ? 〈ge, Callstate f (nil ?) m Kstop〉.
     283  OK ? (Callstate f (nil ?) m Kstop).
    281284
    282285definition Cminor_fullexec : fullexec io_out io_in ≝
    283   mk_fullexec … Cminor_exec ? make_initial_state.
    284 
    285 definition make_initial_noinit_state : Cminor_noinit_program → res (genv × state) ≝
     286  mk_fullexec … Cminor_exec make_global make_initial_state.
     287
     288definition make_noinit_global : Cminor_noinit_program → genv ≝
     289λp. globalenv Genv ?? (λx.[Init_space x]) p.
     290
     291definition make_initial_noinit_state : Cminor_noinit_program → res state ≝
    286292λp.
    287   do ge ← globalenv Genv ?? (λx.[Init_space x]) p;
     293  let ge ≝ make_noinit_global p in
    288294  do m ← init_mem Genv ?? (λx.[Init_space x]) p;
    289295  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
    290296  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
    291   OK ? 〈ge, Callstate f (nil ?) m Kstop〉.
     297  OK ? (Callstate f (nil ?) m Kstop).
    292298
    293299definition Cminor_noinit_fullexec : fullexec io_out io_in ≝
    294   mk_fullexec … Cminor_exec ? make_initial_noinit_state.
     300  mk_fullexec … Cminor_exec make_noinit_global make_initial_noinit_state.
Note: See TracChangeset for help on using the changeset viewer.