Changeset 1376 for src/RTL/semantics.ma


Ignore:
Timestamp:
Oct 14, 2011, 5:55:04 PM (9 years ago)
Author:
sacerdot
Message:

Stack deallocation for RTL implemented in pop_frame.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/semantics.ma

    r1372 r1376  
    5959        (set_sp … (fr_sp hd)
    6060         (set_pc … (fr_pc hd)
    61           (set_carry … (fr_carry hd) st))))) ].
     61          (set_carry … (fr_carry hd)
     62           (set_m … (free … (m … st) (pblock (sp … st))) st)))))) ].
    6263
    6364definition rtl_save_frame:
     
    7778      (set_m … mem
    7879       (set_sp … (mk_pointer XData b ? (mk_offset 0)) st)))).
    79 cases daemon (*CSC: XXXX*)
     80cases daemon (*CSC: XXXX easy lemma on alloc to be turned into a dependent type*)
    8081qed.
    81 
    82 (*+ USARE GLI ARGSNO CHE SONO IN VERITA' I VALORI DEI PARAMETRI COME IN RTLABS
    83 + ALLOCARE LO STACK FRAME*)
    8482
    8583definition rtl_more_sem_params1 : more_sem_params1 … rtl_params1 ≝
Note: See TracChangeset for help on using the changeset viewer.