Ignore:
Timestamp:
Sep 15, 2011, 6:05:31 PM (8 years ago)
Author:
sacerdot
Message:

ERTL ported to the new joint syntax.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r1217 r1220  
    307307  mk_execstep … (is_final globals p exit registersno) (m p) (eval_statement globals p).
    308308
    309 (* CSC: XXX the program type does not fit with the globalenv and init_mem *)
    310 axiom make_initial_state : ∀globals:list ident.∀sparams: sem_params2 globals. joint_program … (pre_sem_params … sparams) → res ((genv … (pre_sem_params … sparams)) × (state sparams)).(* ≝
    311 λp.
    312   do ge ← globalenv Genv ?? p;
    313   do m ← init_mem Genv ?? p;
    314   let main ≝ rtl_pr_main ?? p in
     309definition make_initial_state :
     310 ∀globals:list ident.∀sparams: sem_params2 globals. joint_program ?? (pre_sem_params ? sparams) →
     311   res ((genv ?? (pre_sem_params ? sparams)) × (state sparams)) ≝
     312λglobals,par,p.
     313  do ge ← globalenv Genv … (λx.[Init_space x]) p;
     314  do m ← init_mem Genv … (λx.[Init_space x]) p;
     315  let main ≝ prog_main … p in
    315316  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
    316317  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
    317   OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.
     318  ?(*
     319  OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉*).
     320(*
     321RTL:
     322 init_prog == init_mem
     323 init_sp: inizializzare lo stack pointer
     324 init_isp: inizializzare l'altro stack pointer
     325 init_renv: inizializzare i registri fisici
     326 init_main_call: chiamata di funzione
     327   --- init_fun_call: cambia fra ERTL e LTL
     328 change_carry: a 0
    318329*)
    319 
    320330definition joint_fullexec :
    321331 ∀globals:list ident. ∀sparams:sem_params2 globals. joint_program globals sparams (pre_sem_params … sparams) → fullexec io_out io_in ≝
Note: See TracChangeset for help on using the changeset viewer.