Changeset 3262 for src/ERTL


Ignore:
Timestamp:
May 9, 2013, 11:31:48 AM (7 years ago)
Author:
piccolo
Message:

reverted status_simulation_utils

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL_semantics.ma

    r3261 r3262  
    8383    (set_regs ERTL_state 〈empty_map …,\snd (regs … st')〉 st')).
    8484
    85 definition callee_values_ok : hw_register_env →
    86    (Σl : list beval.|l| = |RegisterCalleeSaved|) → bool ≝
    87 λregs,l.
    88 foldl … andb true
    89  (map2 … (λr : Register.λbv :beval.eq_beval (hwreg_retrieve regs r) bv)
    90   RegisterCalleeSaved l ?).
    91 @hide_prf >(pi2 … l) % qed.
     85definition callee_values_ok : hw_register_env → list beval → bool ≝
     86λregs,l.true (*waiting for Paolo's function*).
    9287
    9388
     
    193188  (* pair_reg_move_     ≝ *) ertl_eval_move
    194189  (* save_frame         ≝ *) ertl_save_frame
    195   (* setup_call         ≝ *) (λgl,ge.λ_.λ_.λ_.λid,st.ertl_setup_call F gl ge id st)
     190  (* setup_call         ≝ *) (λn.λ_.λ_.λst.ertl_setup_call n st)
    196191  (* fetch_external_args≝ *) ertl_fetch_external_args
    197192  (* set_result         ≝ *) ertl_set_result
Note: See TracChangeset for help on using the changeset viewer.