Changeset 1390 for src/LIN


Ignore:
Timestamp:
Oct 17, 2011, 11:43:52 AM (8 years ago)
Author:
sacerdot
Message:

All fetch_result implementations have been factorized out, leaving only a
result_regs function. All axioms in joint_LTL_LIN_semantics but the ones for
external functions have been implemented.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/joint_LTL_LIN_semantics.ma

    r1386 r1390  
    3636 λ_.λ_.λ_.λl.λ_.λ_.λ_.λ_.λst.save_ra … st l.
    3737
    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 *)
     39definition ltl_lin_result_regs:
    4040 ∀succT,succ,pointer_of_label,codeT,lookup.
    4141 ∀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.
    4344
    4445(*CSC: XXXX, for external functions only*)
     
    5556 λsuccT,succ,pointer_of_label,codeT,lookup,fetch,globals.
    5657  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 …)
    5859   ltl_lin_init_locals (ltl_lin_save_frame …) (ltl_lin_pop_frame …)
    5960   (ltl_lin_fetch_external_args …) (ltl_lin_set_result …) (ltl_lin_exec_extended …).
Note: See TracChangeset for help on using the changeset viewer.