Changeset 1372 for src/RTL/semantics.ma


Ignore:
Timestamp:
Oct 14, 2011, 2:48:34 PM (9 years ago)
Author:
sacerdot
Message:

save_frame now takes the stacksize to allow RTL to allocate the stack frame

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/semantics.ma

    r1371 r1372  
    6262
    6363definition rtl_save_frame:
    64  list register → list register → list register → state … rtl_sem_params → res (state … rtl_sem_params) ≝
    65  λformal_arg_regs,actual_arg_regs,retregs,st.
     64 nat → list register → list register → list register → state … rtl_sem_params → res (state … rtl_sem_params) ≝
     65 λstacksize,formal_arg_regs,actual_arg_regs,retregs,st.
     66  let 〈mem,b〉 ≝ alloc … (m … st) 0 stacksize XData in
    6667  do new_regs ←
    6768   mfold_left2 …
     
    7374   (set_frms rtl_sem_params
    7475    (mk_frame retregs (pc … st) (sp … st) (carry … st) (regs … st) :: (st_frms … st))
    75      (set_regs rtl_sem_params new_regs st)).
     76     (set_regs rtl_sem_params new_regs
     77      (set_m … mem
     78       (set_sp … (mk_pointer XData b ? (mk_offset 0)) st)))).
     79cases daemon (*CSC: XXXX*)
     80qed.
    7681
    7782(*+ USARE GLI ARGSNO CHE SONO IN VERITA' I VALORI DEI PARAMETRI COME IN RTLABS
Note: See TracChangeset for help on using the changeset viewer.