Changeset 2954 for src/ERTLptr


Ignore:
Timestamp:
Mar 26, 2013, 3:52:39 PM (7 years ago)
Author:
tranquil
Message:

resolved circular dependency for ERTLptr's semantics

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptr_semantics.ma

    r2946 r2954  
    1717
    1818definition eval_ertlptr_seq:
    19  ∀F. ∀globals. genv_gen F globals →
     19 ∀F.∀globals. genv_gen F globals →
    2020  ertlptr_seq → ident → state ERTL_state →
    2121   res (state ERTL_state) ≝
     
    2323  match stm with
    2424   [ ertlptr_ertl seq ⇒ eval_ertl_seq F globals ge seq id st
    25    | LOW_ADDRESS r l ⇒  ! pc_lab ← get_pc_from_label … ge id l;
     25   | LOW_ADDRESS r l ⇒  ! pc_lab ← gen_pc_from_label … ge id l;
    2626                        let 〈addrl,addrh〉 ≝ beval_pair_of_pc pc_lab in
    2727                        ps_reg_store_status r addrl st
    28    | HIGH_ADDRESS r l ⇒ ! pc_lab ← get_pc_from_label … ge id l;
     28   | HIGH_ADDRESS r l ⇒ ! pc_lab ← gen_pc_from_label … ge id l;
    2929                        let 〈addrl,addrh〉 ≝  beval_pair_of_pc pc_lab in
    3030                        ps_reg_store_status r addrh st
Note: See TracChangeset for help on using the changeset viewer.