Changeset 2808 for src/RTLabs


Ignore:
Timestamp:
Mar 7, 2013, 6:03:18 PM (7 years ago)
Author:
tranquil
Message:

added local_stacksize to joint internal functions to accomodate for locals in the stack inherited from the front end

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL.ma

    r2774 r2808  
    124124    mk_joint_internal_function RTL globals
    125125      (joint_if_luniverse … def') (joint_if_runiverse … def') ret'
    126       params' (joint_if_stacksize … def')
     126      params' (joint_if_stacksize … def') (joint_if_local_stacksize … def')
    127127      (joint_if_code … def') (joint_if_entry … def') in
    128128   〈def'', lenv〉. @hide_prf
     
    284284  | Oaddrsymbol id offset ⇒ λcst_prf,prf.
    285285    let 〈r1, r2〉 ≝ make_addr … destrs ? in
    286     [ADDRESS RTL globals id ? r1 r2]
     286    [ADDRESS RTL globals id ? r1 r2 ;
     287     r1 ← r1 .Add. byte_of_nat … offset ;
     288     r2 ← r2 .Addc. zero_byte ]
    287289  | Oaddrstack offset ⇒ λcst_prf,prf.
    288290    let 〈r1, r2〉 ≝ make_addr … destrs ? in
    289     [(rtl_stack_address r1 r2 : joint_seq RTL globals)]
     291    [(rtl_stack_address r1 r2 : joint_seq RTL globals);
     292     r1 ← r1 .Add. byte_of_nat … offset ;
     293     r2 ← r2 .Addc. zero_byte ]
    290294  ] (pi2 … cst_sig).
    291295  @hide_prf
     
    10321036  let entry' ≝ f_entry def in
    10331037  let init ≝ mk_joint_internal_function RTL globals
    1034     luniverse' runiverse' [ ] [ ] stack_size'
     1038    luniverse' runiverse' [ ] [ ] stack_size' stack_size'
    10351039    (add … (empty_map ? (joint_statement ??)) entry' (RETURN …)) (pi1 … entry') in
    10361040  let 〈init',lenv〉 as pr_eq ≝ initialize_locals_params_ret globals
Note: See TracChangeset for help on using the changeset viewer.