Ignore:
Timestamp:
Feb 19, 2013, 12:23:50 PM (7 years ago)
Author:
campbell
Message:

Retain the pointer for the function called in front-end call states
so that we can do sensible stack costs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/switchRemoval.ma

    r2608 r2677  
    19871987      (State sss_func_tr sss_result sss_k_ext sss_env_ext sss_m_ext)
    19881988| sws_callstate :
     1989 ∀ssc_vf.
    19891990 ∀ssc_fd.
    19901991 ∀ssc_args.
     
    19992000    switch_cont_sim (\snd (function_switch_removal ssc_f)) ssc_k ssc_k_ext
    20002001  | _ ⇒ True ]) →
    2001     switch_state_sim ge (Callstate ssc_fd ssc_args ssc_k ssc_m)
    2002                         (Callstate (fundef_switch_removal ssc_fd) ssc_args ssc_k_ext ssc_m_ext)
     2002    switch_state_sim ge (Callstate ssc_vf ssc_fd ssc_args ssc_k ssc_m)
     2003                        (Callstate ssc_vf (fundef_switch_removal ssc_fd) ssc_args ssc_k_ext ssc_m_ext)
    20032004| sws_returnstate :
    20042005 ∀ssr_result.
Note: See TracChangeset for help on using the changeset viewer.