- Timestamp:
- Oct 19, 2011, 11:30:24 AM (9 years ago)
- Location:
- src/LIN
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/LIN/joint_LTL_LIN_semantics.ma
r1390 r1408 6 6 λsuccT,succ,pointer_of_label. 7 7 mk_more_sem_params ? 8 unit hw_register_envsucc8 unit it hw_register_env empty_hw_register_env 0 it succ 9 9 hwreg_store hwreg_retrieve (λ_.hwreg_store RegisterA) (λe.λ_.hwreg_retrieve e RegisterA) 10 10 (λ_.hwreg_store RegisterB) (λe.λ_.hwreg_retrieve e RegisterB) -
src/LIN/semantics.ma
r1383 r1408 5 5 λ_.λaddr. addr_add addr 1. 6 6 7 (*CSC: XXXX here re-use the code for the lookup argument of LIN params__ *) 7 8 axiom lin_pointer_of_label: label → Σp:pointer. ptype p = Code. 8 9 9 axiom NotFound: String. 10 (*CSC: XXX factorize code with graph_fetch_statement!!!!!*) 11 axiom BadProgramCounter: String. 10 12 axiom lin_fetch_statement: 11 ∀globals. genv … (lin_params globals) → state (ltl_lin_sem_params … lin_succ_pc lin_pointer_of_label) → res (pre_lin_statement globals).(* ≝ 12 λglobals,ge,st. 13 let pc ≝ pc … st in 14 ?. 15 let fn ≝ ? in 16 opt_to_res ? [MSG NotFound] (lookup … (lin_params …) (joint_if_code … fn) ?(*label???*)). 17 *) 13 ∀globals. genv … (lin_params globals) → state (ltl_lin_sem_params … lin_succ_pc lin_pointer_of_label) → res (pre_lin_statement globals). 14 (* λglobals,ge,st. 15 do p ← pointer_of_address (pc … st) ; 16 let b ≝ pblock p in 17 do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ; 18 [ Internal def' ⇒ 19 let off ≝ poff p in 20 opt_to_res ? [MSG BadProgramCounter] (\snd (nth ?? (joint_if_code … def') off)) 21 | External _ ⇒ Error … [MSG BadProgramCounter]].*) 18 22 19 23 definition lin_fullexec ≝ ltl_lin_fullexec … lin_succ_pc lin_pointer_of_label … lin_fetch_statement.
Note: See TracChangeset
for help on using the changeset viewer.