Ignore:
Timestamp:
May 9, 2013, 12:49:38 AM (6 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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/joint_LTL_LIN_semantics.ma

    r3037 r3259  
    8686  (* allocate_local     ≝ *) (λabs.match abs in void with [ ])
    8787*)  (* save_frame         ≝ *) LTL_LIN_save_frame
    88   (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
     88  (* setup_call         ≝ *) (λ_.λ_.λ_.λ_.λ_.λ_.λst.return st)
    8989  (* fetch_external_args≝ *) ltl_lin_fetch_external_args
    9090  (* set_result         ≝ *) ltl_lin_set_result
Note: See TracChangeset for help on using the changeset viewer.