Changeset 2722 for src/Clight/switchRemoval.ma

Timestamp:

Feb 23, 2013, 5:05:03 PM (7 years ago)

Author:

campbell

Message:

It's easier to keep the real function identifier in front-end Callstates
than mucking around with the function pointer.

File:

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

src/Clight/switchRemoval.ma

@@ -1923 +1923 @@
   rg_find_symbol: ∀s.
     find_symbol ? ge s = find_symbol ? ge' s;
-  rg_find_funct: ∀v,f.
-    find_funct ? ge v = Some ? f →
-    find_funct ? ge' v = Some ? (t f);
+  rg_find_funct_id: ∀v,f,id.
+    find_funct_id ? ge v = Some ? 〈f,id〉 →
+    find_funct_id ? ge' v = Some ? 〈t f,id〉;
   rg_find_funct_ptr: ∀b,f.
     find_funct_ptr ? ge b = Some ? f →
@@ -2913 +2913 @@
        cases (bindIO_inversion ??????? Hexec) #xfunc * #Heq_func #Hexec_func
        cases (bindIO_inversion ??????? Hexec_func) #xargs * #Heq_args #Hexec_args
-       cases (bindIO_inversion ??????? Hexec_args) #called_fundef * #Heq_fundef #Hexec_typeeq
+       cases (bindIO_inversion ??????? Hexec_args) * #called_fundef #fid * #Heq_fundef #Hexec_typeeq
        cases (bindIO_inversion ??????? Hexec_typeeq) #Htype_eq * #Heq_assert #Hexec_ret
        >(Hsim_expr … Heq_func) whd in match (m_bind ?????);
        >(exec_expr_sim_to_exec_exprlist … Hsim_expr … Heq_args)
        whd in ⊢ (??%?);
-       >(rg_find_funct … Hrelated … (opt_to_io_Value … Heq_fundef))
+       >(rg_find_funct_id … Hrelated … (opt_to_io_Value … Heq_fundef))
        whd in ⊢ (??%?); <fundef_type_simplify >Heq_assert
        whd in ⊢ (??%?); -Hexec -Hexec_func -Hexec_args -Hexec_typeeq lapply Hexec_ret -Hexec_ret