Changeset 1303


Ignore:
Timestamp:
Oct 6, 2011, 12:16:22 AM (8 years ago)
Author:
sacerdot
Message:
  1. LTL/semantics.ma added (work in progress)
  2. init_locals fixed to take in input the old register environment, since physical registers should just be left untouched
Location:
src
Files:
1 added
3 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1302 r1303  
    33
    44(*CSC: XXXXX *)
    5 axiom ertl_init_locals : list register → (register_env beval) × hw_register_env.
     5axiom ertl_init_locals : list register → (register_env beval) × hw_register_env → (register_env beval) × hw_register_env.
    66axiom ertl_pop_frame: unit → res unit.
    77axiom ertl_save_frame: unit → (register_env beval) × hw_register_env → unit.
  • src/RTL/semantics.ma

    r1301 r1303  
    1010
    1111(*CSC: XXXXX *)
    12 axiom rtl_init_locals : list register → register_env beval.
     12axiom rtl_init_locals : list register → register_env beval → register_env beval.
    1313axiom rtl_pop_frame: unit → res unit.
    1414axiom rtl_save_frame: unit → register_env beval → unit.
  • src/joint/semantics.ma

    r1298 r1303  
    5858 { more_sparams:> more_sem_params p
    5959
    60  ; init_locals : localsT p → regsT … more_sparams
     60 ; init_locals : localsT p → regsT … more_sparams → regsT … more_sparams
    6161 
    6262 ; fetch_statement: genv … p → state (mk_sem_params … more_sparams) → res (joint_statement (mk_sem_params … more_sparams) globals)
     
    289289            ! st ← save_ra … st l;
    290290              let st ≝ save_frame … st in
    291               let regs ≝ init_locals … (joint_if_locals … fn) in
     291              let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
    292292              let l' ≝ joint_if_entry … fn in
    293293             ret ? 〈 E0, goto … l' (set_regs p regs st)〉
Note: See TracChangeset for help on using the changeset viewer.