Changeset 1312 for src/ERTL


Ignore:
Timestamp:
Oct 6, 2011, 10:35:29 PM (9 years ago)
Author:
sacerdot
Message:

Type of frame operations (pop_frame/save_frame) generalized to take in account
the RTL semantics. LTL and LIN semantics fixed. Fixing of ERTL/RTL still to
be done.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ERTL/semantics.ma

    r1303 r1312  
    44(*CSC: XXXXX *)
    55axiom ertl_init_locals : list register → (register_env beval) × hw_register_env → (register_env beval) × hw_register_env.
    6 axiom ertl_pop_frame: unit → res unit.
     6NON BASTA: DEBBO RIPRISTINARE IL LOCAL_ENV E IN RTL TANTE COSE!
     7axiom ertl_pop_frame: list (register_env beval) → res (list (register_env beval)).
    78axiom ertl_save_frame: unit → (register_env beval) × hw_register_env → unit.
    89
    … …  
    2526definition ertl_more_sem_params: more_sem_params ertl_params_ :=
    2627 mk_more_sem_params ertl_params_
    27   unit(*framesT*) ((register_env beval) × hw_register_env) graph_succ_p ertl_pop_frame ertl_save_frame
     28  (list (register_env beval)) ((register_env beval) × hw_register_env) graph_succ_p ertl_pop_frame ertl_save_frame
    2829   ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
    2930    ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
Note: See TracChangeset for help on using the changeset viewer.