Changeset 1390 for src/LIN

Timestamp:

Oct 17, 2011, 11:43:52 AM (9 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:

• src/LIN/joint_LTL_LIN_semantics.ma (modified) (2 diffs)

src/LIN/joint_LTL_LIN_semantics.ma

@@ -36 +36 @@
  λ_.λ_.λ_.λl.λ_.λ_.λ_.λ_.λst.save_ra … st l.
 
-(*CSC: XXXXX, for is_final only *)
-axiom ltl_lin_fetch_result:
+(* The following implementation only works for functions that return 32 bits *)
+definition ltl_lin_result_regs:
  ∀succT,succ,pointer_of_label,codeT,lookup.
  ∀globals. genv globals (mk_params globals succT ltl_lin_params1 (codeT globals) (lookup globals)) →
- state (ltl_lin_sem_params succT succ pointer_of_label) → res (list beval).
+ state (ltl_lin_sem_params succT succ pointer_of_label) → res (list Register) ≝
+ λ_.λ_.λ_.λ_.λ_.λ_.λ_.λ_. OK … RegisterRets.
 
 (*CSC: XXXX, for external functions only*)
@@ -55 +56 @@
  λsuccT,succ,pointer_of_label,codeT,lookup,fetch,globals.
   mk_more_sem_params2 … (ltl_lin_more_sem_params … succ pointer_of_label)
-   (fetch globals) (load_ra …) (ltl_lin_fetch_result …)
+   (fetch globals) (load_ra …) (ltl_lin_result_regs …)
    ltl_lin_init_locals (ltl_lin_save_frame …) (ltl_lin_pop_frame …)
    (ltl_lin_fetch_external_args …) (ltl_lin_set_result …) (ltl_lin_exec_extended …).