Changeset 2991 for src/ERTL

Timestamp:

Mar 27, 2013, 9:57:13 PM (7 years ago)

Author:

piccolo

Message:

Fixed cond and seq case in StatusSimulationHelper?

Added cost case in StatusSimulationHelper?

File:

• src/ERTL/ERTLtoERTLptrOK.ma (modified) (2 diffs)

src/ERTL/ERTLtoERTLptrOK.ma

@@ -165 +165 @@
 definition state_rel ≝ λprog : ertl_program.λf_lbls.
 λf_regs : (block → label → list register).
-λbl.λ_:label.λst1,st2.∃f,fn.
+λbl.λ_ : label.λst1,st2.∃f,fn.
 fetch_internal_function ? (globalenv_noinit … prog) bl = return 〈f,fn〉 ∧ 
 let added ≝ added_registers ERTL (prog_var_names … prog) fn (f_regs bl) in 
@@ -842 +842 @@
        >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]));
        >EQfetch' in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?])); normalize nodelta
+       >(fetch_stmt_ok_sigma_state_ok … EQfetch) >EQc_bl >m_return_bind
+       lapply EQc_bl' whd in match block_of_call; normalize nodelta
        cases daemon (* CSC: The proof used to be %, why did it change? *)
+                    (* This point will be generalized when the call case
+                       will be available in StatusSimulationHelper*)
        (*
        XXX