Ignore:
Timestamp:
May 9, 2013, 12:49:38 AM (6 years ago)
Author:
piccolo
Message:

changed ERTL semantics:
1) added manipulation of stack pointer directly in the semantics
2) added values of Callee Saved in frames

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/StatusSimulationUtils.ma

    r3154 r3259  
    419419  ∀n.stack_sizes f1 = return n → 
    420420  ∀st1'.
    421   setup_call ?? P_in n (joint_if_params … fn1) arg st1_pre = return 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' →
    422423  st_rel st1 st2 → 
    423424  ∀t_fn1.
     
    444445         (mk_state_pc ? st2_pre_call pc' (last_pop … st2)) = return st2_pre ∧
    445446       ∃st2_after_call.
    446          setup_call ?? P_out n (joint_if_params … t_fn1) arg' st2_pre
     447         setup_call ?? P_out … (joint_globalenv P_out trans_prog stack_sizes) … n
     448          (joint_if_params … t_fn1) arg' f1 st2_pre
    447449          = return st2_after_call ∧
    448450       bind_new_P' ??
     
    515517   ∀ssize_f1.stack_sizes f1 = return ssize_f1 →   
    516518   ∀st1'.
    517     setup_call ?? P_in ssize_f1 (joint_if_params … fn1) arg
     519    setup_call ?? P_in … (joint_globalenv P_in prog stack_sizes) … ssize_f1
     520     (joint_if_params … fn1) arg f1
    518521     (decrement_stack_usage P_in ssize_f (st_no_pc … st1)) = return st1' →
    519522   st_rel st1 st2 → 
     
    533536         st2_pre_call = return bl ∧
    534537       ∃st2_after.
    535         setup_call ?? P_out ssize_f1 (joint_if_params … t_fn1) arg'
     538        setup_call ?? P_out … (joint_globalenv P_out trans_prog stack_sizes) …
     539         ssize_f1 (joint_if_params … t_fn1) arg' f1
    536540         (decrement_stack_usage P_out ssize_f st2_pre_call) = return st2_after ∧
    537541       bind_new_P' ??
Note: See TracChangeset for help on using the changeset viewer.