Changeset 1322


Ignore:
Timestamp:
Oct 7, 2011, 2:59:48 PM (8 years ago)
Author:
sacerdot
Message:

address => stack_address

Location:
src/RTL
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL.ma

    r1280 r1322  
    55  To be fixed once we understand exactly what to do with tail calls. *)
    66inductive rtl_statement_extension: Type[0] ≝
    7   | rtl_st_ext_address: register → register → rtl_statement_extension
     7  | rtl_st_ext_stack_address: register → register → rtl_statement_extension
    88  | rtl_st_ext_call_ptr: register → register → list register → list register → rtl_statement_extension
    99  | rtl_st_ext_tailcall_id: ident → list register → rtl_statement_extension
  • src/RTL/RTLToERTL.ma

    r1315 r1322  
    309309         match ext with
    310310          [ rtlntc_st_ext_call_ptr _ _ _ _ ⇒ ⊥ (*CSC: XXXX not implemented in OCaml too *)
    311           | rtlntc_st_ext_address r1 r2 ⇒
     311          | rtlntc_st_ext_stack_address r1 r2 ⇒
    312312             adds_graph ertl_params1 … [
    313313              sequential ertl_params_ … (MOVE … 〈pseudo r1, hardware RegisterSPL〉);
  • src/RTL/semantics.ma

    r1320 r1322  
    6565axiom rtl_set_result: list val → state rtl_sem_params → res (state rtl_sem_params).
    6666
    67 axiom rtl_exec_extended: ∀globals. genv globals (rtl_params globals) → rtl_statement_extension → state rtl_sem_params → IO io_out io_in (trace × (state rtl_sem_params)).
     67definition rtl_exec_extended:
     68 ∀globals. genv globals (rtl_params globals) →
     69  rtl_statement_extension → state rtl_sem_params →
     70   IO io_out io_in (trace × (state rtl_sem_params)) ≝
     71 λglobals,ge,stm,st.
     72  match stm with
     73   [ rtl_st_ext_address dreg sreg ⇒
     74     
     75   | rtl_st_ext_call_ptr _ _ _ _ ⇒ ?
     76   | rtl_st_ext_tailcall_id id regs ⇒ ?
     77   | rtl_st_ext_tailcall_ptr _ _ _ ⇒ ?
     78   ].
    6879
    6980definition rtl_more_sem_params2: ∀globals. more_sem_params2 … (rtl_params globals) ≝
Note: See TracChangeset for help on using the changeset viewer.