Changeset 1303 for src/ERTL


Ignore:
Timestamp:
Oct 6, 2011, 12:16:22 AM (9 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
File:
1 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.
Note: See TracChangeset for help on using the changeset viewer.