- Timestamp:
- Oct 17, 2011, 11:43:52 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/LIN/joint_LTL_LIN_semantics.ma
r1386 r1390 36 36 λ_.λ_.λ_.λl.λ_.λ_.λ_.λ_.λst.save_ra … st l. 37 37 38 (* CSC: XXXXX, for is_final only*)39 axiom ltl_lin_fetch_result:38 (* The following implementation only works for functions that return 32 bits *) 39 definition ltl_lin_result_regs: 40 40 ∀succT,succ,pointer_of_label,codeT,lookup. 41 41 ∀globals. genv globals (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) → 42 state (ltl_lin_sem_params succT succ pointer_of_label) → res (list beval). 42 state (ltl_lin_sem_params succT succ pointer_of_label) → res (list Register) ≝ 43 λ_.λ_.λ_.λ_.λ_.λ_.λ_.λ_. OK … RegisterRets. 43 44 44 45 (*CSC: XXXX, for external functions only*) … … 55 56 λsuccT,succ,pointer_of_label,codeT,lookup,fetch,globals. 56 57 mk_more_sem_params2 … (ltl_lin_more_sem_params … succ pointer_of_label) 57 (fetch globals) (load_ra …) (ltl_lin_ fetch_result…)58 (fetch globals) (load_ra …) (ltl_lin_result_regs …) 58 59 ltl_lin_init_locals (ltl_lin_save_frame …) (ltl_lin_pop_frame …) 59 60 (ltl_lin_fetch_external_args …) (ltl_lin_set_result …) (ltl_lin_exec_extended …).
Note: See TracChangeset
for help on using the changeset viewer.