Changeset 1322 for src/RTL/semantics.ma


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

address => stack_address

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.