Changeset 1372 for src/joint


Ignore:
Timestamp:
Oct 14, 2011, 2:48:34 PM (8 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/joint/semantics.ma

    r1371 r1372  
    5353   (*CSC: save_frame returns a res only because we can call a function with the wrong number and
    5454     type of arguments. To be fixed using a dependent type *)
    55  ; save_frame: paramsT … p → call_args p → call_dest p → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
     55 ; save_frame: nat → paramsT … p → call_args p → call_dest p → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
    5656 }.
    5757
     
    294294          [ Internal fn ⇒
    295295            ! st ← save_ra … st l;
    296             ! st ← save_frame … (joint_if_params … fn) args dest st ;
     296            ! st ← save_frame … (joint_if_stacksize … fn) (joint_if_params … fn) args dest st ;
    297297            let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
    298298            let l' ≝ joint_if_entry … fn in
Note: See TracChangeset for help on using the changeset viewer.