Ignore:
Timestamp:
Nov 8, 2012, 2:27:54 PM (7 years ago)
Author:
tranquil
Message:

changed joint's stack pointer and internal stack

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/joint_LTL_LIN_semantics.ma

    r2286 r2443  
    2727 (* empty_framesT ≝ *) it
    2828 (* regsT ≝ *) hw_register_env
    29  (* empty_regsT ≝ *) init_hw_register_env.
     29 (* empty_regsT ≝ *) init_hw_register_env
     30 (* load_sp ≝ *) hwreg_retrieve_sp
     31 (* store_sp ≝ *) hwreg_store_sp.
    3032
    3133(*CSC: XXXX, for external functions only*)
     
    3739
    3840definition LTL_LIN_semantics ≝
    39   λF.mk_more_sem_unserialized_params LTL_LIN F
     41  λF.mk_sem_unserialized_params LTL_LIN F
    4042  (* st_pars            ≝ *) LTL_LIN_state
    4143  (* acca_store_        ≝ *) (λ_.hw_reg_store RegisterA)
Note: See TracChangeset for help on using the changeset viewer.