Changeset 2537 for src/LIN


Ignore:
Timestamp:
Dec 6, 2012, 1:24:29 PM (7 years ago)
Author:
tranquil
Message:

rolled back changes on calls in joint. Now the save_frame parameter
has a switch that tells whether the call is an ident one or a pointer one.
The idea is that in the latter case, from LTL onwards, the caller address is not saved (as it is done by explicit instructions

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/joint_LTL_LIN.ma

    r2490 r2537  
    1010inductive ltl_lin_seq : Type[0] ≝
    1111| SAVE_CARRY : ltl_lin_seq
    12 | RESTORE_CARRY : ltl_lin_seq.
     12| RESTORE_CARRY : ltl_lin_seq
     13| LOW_ADDRESS : Register → label → ltl_lin_seq
     14| HIGH_ADDRESS : Register → label → ltl_lin_seq.
     15
     16definition ltl_lin_seq_labels ≝ λs.match s with
     17[ LOW_ADDRESS _ lbl ⇒ [ lbl ]
     18| HIGH_ADDRESS _ lbl ⇒ [ lbl ]
     19| _ ⇒ [ ]
     20].
    1321
    1422definition LTL_LIN : unserialized_params ≝ mk_unserialized_params
     
    2634    (* call_dest ≝ *) unit
    2735    (* ext_seq ≝ *) ltl_lin_seq
     36    (* ext_seq_labels ≝ *) ltl_lin_seq_labels
    2837    (* has_tailcalls ≝ *) false
    2938    (* paramsT ≝ *) unit
Note: See TracChangeset for help on using the changeset viewer.