Changeset 2808 for src/joint/Joint.ma


Ignore:
Timestamp:
Mar 7, 2013, 6:03:18 PM (8 years ago)
Author:
tranquil
Message:

added local_stacksize to joint internal functions to accomodate for locals in the stack inherited from the front end

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2783 r2808  
    475475  joint_if_result   : call_dest p;
    476476  joint_if_params   : paramsT p;
    477 (*CSC: XXXXX stacksize unused for LTL-...*)
    478477  joint_if_stacksize: nat;
     478  joint_if_local_stacksize: nat; (* size of the stack devoted to "forced" stack positions
     479    (that are already on stack in the front end) *)
    479480  joint_if_code     : codeT p globals ;
    480481  joint_if_entry : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) (*;
     
    552553      (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun)
    553554      (joint_if_params … int_fun) (joint_if_stacksize … int_fun)
     555       (joint_if_local_stacksize … int_fun)
    554556      graph entry (*exit*).
    555557
     
    571573   mk_joint_internal_function globals pars
    572574    luniverse (joint_if_runiverse … p) (joint_if_result … p)
    573     (joint_if_params … p) (joint_if_stacksize … p)
     575    (joint_if_params … p) (joint_if_stacksize … p) (joint_if_local_stacksize … p)
    574576    (joint_if_code … p) (joint_if_entry … p) (*(joint_if_exit … p)*).
    575577
     
    580582   mk_joint_internal_function globals pars
    581583    (joint_if_luniverse … p) runiverse (joint_if_result … p)
    582     (joint_if_params … p) (joint_if_stacksize … p)
     584    (joint_if_params … p) (joint_if_stacksize … p) (joint_if_local_stacksize … p)
    583585    (joint_if_code … p) (joint_if_entry … p) (*(joint_if_exit … p)*).
    584586   
     
    590592    mk_joint_internal_function …
    591593     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    592      (joint_if_params … p) (joint_if_stacksize … p)
     594     (joint_if_params … p) (joint_if_stacksize … p) (joint_if_local_stacksize … p)
    593595     code
    594596     (pi1 … (joint_if_entry … p))
Note: See TracChangeset for help on using the changeset viewer.