Changeset 3263 for src/RTLabs


Ignore:
Timestamp:
May 10, 2013, 1:40:31 PM (6 years ago)
Author:
tranquil
Message:

moved callee saved saving and restoring to ERTL -> LTL pass (untrusted
colourer and interference graph creator still need to be updated)
joint now has the stack size split in three (referenced locals, params
and spilled)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL.ma

    r3145 r3263  
    132132    mk_joint_internal_function RTL globals
    133133      (joint_if_luniverse … def') (joint_if_runiverse … def') ret'
    134       params' (joint_if_stacksize … def') (joint_if_local_stacksize … def')
     134      params' (joint_if_stacksize … def') (joint_if_local_stacksize … def') 0
    135135      (joint_if_code … def') (joint_if_entry … def') in
    136136   〈def'', lenv〉. @hide_prf
     
    10851085  let entry' ≝ pi1 … (f_entry def) in
    10861086  let init ≝ mk_joint_internal_function RTL globals
    1087     luniverse' runiverse' [ ] [ ] 0 0
     1087    luniverse' runiverse' [ ] [ ] 0 0 0
    10881088    (add … (empty_map ? (joint_statement ??)) entry' (RETURN …)) entry' in
    10891089  let 〈init',lenv〉 as pr_eq ≝ initialize_locals_params_ret globals
     
    11031103    (joint_if_result … def)
    11041104    (joint_if_params … def)
    1105     stack_size' stack_size'
     1105    stack_size' 0 0
    11061106    (joint_if_code … def)
    11071107    (joint_if_entry … def).
     
    11451145  ** #H %{H} % ]
    11461146@All2_of_map * #id * #f normalize nodelta [2: %]
    1147 % [%] whd in match translate_internal; normalize nodelta
     1147% [%] whd in match translate_internal; whd in match joint_if_stacksize;
     1148normalize nodelta
    11481149cases (initialize_locals_params_ret ?????) normalize nodelta #a #b %1
    11491150qed.
Note: See TracChangeset for help on using the changeset viewer.