Ignore:
Timestamp:
May 9, 2013, 12:49:38 AM (6 years ago)
Author:
piccolo
Message:

changed ERTL semantics:
1) added manipulation of stack pointer directly in the semantics
2) added values of Callee Saved in frames

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/joint_semantics.ma

    r3154 r3259  
    221221   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
    222222     type of arguments. To be fixed using a dependent type *)
    223   ; setup_call : nat → paramsT … uns_pars → call_args uns_pars →
     223  ; setup_call : ∀globals.∀ge : genv_gen F globals.nat → paramsT … uns_pars → call_args uns_pars → ident →
    224224      state st_pars → res (state st_pars)
    225225  ; fetch_external_args: external_function → state st_pars → call_args … uns_pars →
     
    585585λst : state p.
    586586! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … i] (stack_sizes … ge i) ;
    587 ! st' ← setup_call … stack_size (joint_if_params … globals fn) args st ;
     587! st' ← setup_call … ge … stack_size (joint_if_params … globals fn) args i st ;
    588588return increment_stack_usage … stack_size st'.
    589589
Note: See TracChangeset for help on using the changeset viewer.