Changeset 2677 for src/Clight/switchRemoval.ma

Timestamp:

Feb 19, 2013, 12:23:50 PM (8 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:

• src/Clight/switchRemoval.ma (modified) (2 diffs)

src/Clight/switchRemoval.ma

@@ -1987 +1987 @@
       (State sss_func_tr sss_result sss_k_ext sss_env_ext sss_m_ext)
 | sws_callstate :
+ ∀ssc_vf.
  ∀ssc_fd.
  ∀ssc_args.
@@ -1999 +2000 @@
     switch_cont_sim (\snd (function_switch_removal ssc_f)) ssc_k ssc_k_ext
   | _ ⇒ True ]) →
-    switch_state_sim ge (Callstate ssc_fd ssc_args ssc_k ssc_m)
-                        (Callstate (fundef_switch_removal ssc_fd) ssc_args ssc_k_ext ssc_m_ext)
+    switch_state_sim ge (Callstate ssc_vf ssc_fd ssc_args ssc_k ssc_m)
+                        (Callstate ssc_vf (fundef_switch_removal ssc_fd) ssc_args ssc_k_ext ssc_m_ext)
 | sws_returnstate :
  ∀ssr_result.