Changeset 2991 for src/ERTL


Ignore:
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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLtoERTLptrOK.ma

    r2943 r2991  
    165165definition state_rel ≝ λprog : ertl_program.λf_lbls.
    166166λf_regs : (block → label → list register).
    167 λbl.λ_:label.λst1,st2.∃f,fn.
     167λbl.λ_ : label.λst1,st2.∃f,fn.
    168168fetch_internal_function ? (globalenv_noinit … prog) bl = return 〈f,fn〉 ∧
    169169let added ≝ added_registers ERTL (prog_var_names … prog) fn (f_regs bl) in
     
    842842       >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]));
    843843       >EQfetch' in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?])); normalize nodelta
     844       >(fetch_stmt_ok_sigma_state_ok … EQfetch) >EQc_bl >m_return_bind
     845       lapply EQc_bl' whd in match block_of_call; normalize nodelta
    844846       cases daemon (* CSC: The proof used to be %, why did it change? *)
     847                    (* This point will be generalized when the call case
     848                       will be available in StatusSimulationHelper*)
    845849       (*
    846850       XXX
Note: See TracChangeset for help on using the changeset viewer.