Changeset 3259 for src/LIN

Timestamp:

May 9, 2013, 12:49:38 AM (8 years ago)

Author:

piccolo

Message:

changed ERTL semantics:
1) added manipulation of stack pointer directly in the semantics
2) added values of Callee Saved in frames

File:

• src/LIN/joint_LTL_LIN_semantics.ma (modified) (1 diff)

src/LIN/joint_LTL_LIN_semantics.ma

@@ -86 +86 @@
   (* allocate_local     ≝ *) (λabs.match abs in void with [ ])
 *)  (* save_frame         ≝ *) LTL_LIN_save_frame
-  (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
+  (* setup_call         ≝ *) (λ_.λ_.λ_.λ_.λ_.λ_.λst.return st)
   (* fetch_external_args≝ *) ltl_lin_fetch_external_args
   (* set_result         ≝ *) ltl_lin_set_result