Changeset 3262


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

reverted status_simulation_utils

Location:
src
Files:
2 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
  • src/joint/StatusSimulationUtils.ma

    r3259 r3262  
    1212(*                                                                        *)
    1313(**************************************************************************)
    14 
     14 
    1515include "joint/semanticsUtils.ma".
    1616include "joint/Traces.ma".
     
    419419  ∀n.stack_sizes f1 = return n → 
    420420  ∀st1'.
    421   setup_call ?? P_in … (joint_globalenv P_in prog stack_sizes) … n (joint_if_params … fn1)
    422    arg f1 st1_pre = return st1' →
     421  setup_call ?? P_in n (joint_if_params … fn1) arg st1_pre = return st1' →
    423422  st_rel st1 st2 → 
    424423  ∀t_fn1.
     
    445444         (mk_state_pc ? st2_pre_call pc' (last_pop … st2)) = return st2_pre ∧
    446445       ∃st2_after_call.
    447          setup_call ?? P_out … (joint_globalenv P_out trans_prog stack_sizes) … n
    448           (joint_if_params … t_fn1) arg' f1 st2_pre
     446         setup_call ?? P_out n (joint_if_params … t_fn1) arg' st2_pre
    449447          = return st2_after_call ∧
    450448       bind_new_P' ??
     
    517515   ∀ssize_f1.stack_sizes f1 = return ssize_f1 →   
    518516   ∀st1'.
    519     setup_call ?? P_in … (joint_globalenv P_in prog stack_sizes) … ssize_f1
    520      (joint_if_params … fn1) arg f1
     517    setup_call ?? P_in ssize_f1 (joint_if_params … fn1) arg
    521518     (decrement_stack_usage P_in ssize_f (st_no_pc … st1)) = return st1' →
    522519   st_rel st1 st2 → 
     
    536533         st2_pre_call = return bl ∧
    537534       ∃st2_after.
    538         setup_call ?? P_out … (joint_globalenv P_out trans_prog stack_sizes) …
    539          ssize_f1 (joint_if_params … t_fn1) arg' f1
     535        setup_call ?? P_out ssize_f1 (joint_if_params … t_fn1) arg'
    540536         (decrement_stack_usage P_out ssize_f st2_pre_call) = return st2_after ∧
    541537       bind_new_P' ??
Note: See TracChangeset for help on using the changeset viewer.