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

    r1139 r1238  
    204204].
    205205
    206 definition RTLabs_exec : execstep io_out io_in ≝
    207   mk_execstep … ? is_final mem_of_state eval_statement.
    208 
    209 definition make_initial_state : RTLabs_program → res (genv × state) ≝
     206definition RTLabs_exec : trans_system io_out io_in ≝
     207  mk_trans_system … ? (λ_.is_final) eval_statement.
     208
     209definition make_global : RTLabs_program → genv ≝
     210λp. globalenv Genv ?? (λx.[Init_space x]) p.
     211
     212definition make_initial_state : RTLabs_program → res state ≝
    210213λp.
    211   do ge ← globalenv Genv ?? (λx.[Init_space x]) p;
     214  let ge ≝ make_global p in
    212215  do m ← init_mem Genv ?? (λx.[Init_space x]) p;
    213216  let main ≝ prog_main ?? p in
    214217  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
    215218  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
    216   OK ? 〈ge,Callstate f (nil ?) (None ?) (nil ?) m〉.
     219  OK ? (Callstate f (nil ?) (None ?) (nil ?) m).
    217220
    218221definition RTLabs_fullexec : fullexec io_out io_in ≝
    219   mk_fullexec … RTLabs_exec ? make_initial_state.
    220 
     222  mk_fullexec … RTLabs_exec make_global make_initial_state.
     223
Note: See TracChangeset for help on using the changeset viewer.