Changeset 1376


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

Stack deallocation for RTL implemented in pop_frame.

Location:
src
Files:
2 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 ≝
  • src/joint/semantics.ma

    r1372 r1376  
    309309          ]]
    310310    | RETURN ⇒
    311 (* + DEALLOCARE LO STACK FRAME*)
    312311      ! res ← fetch_result … st;
    313312      ! st ← pop_frame … res st;
Note: See TracChangeset for help on using the changeset viewer.