Changeset 1329 for src/ERTL/semantics.ma


Ignore:
Timestamp:
Oct 7, 2011, 6:19:41 PM (9 years ago)
Author:
sacerdot
Message:
  1. Definition of addresses moved to BEMem
  2. Basic functions on addresses implemented in BEMem and used everywhere
  3. Semantics of ERTL extended statements completed
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1327 r1329  
    9494      ! v ← framesize globals st;
    9595      ! sp ← get_hwsp st;
    96         let newsp ≝ ?(*addr_sub sp v*) in
     96      ! newsp ← addr_sub sp v;
    9797      ! st ← set_hwsp newsp st;
    9898        ret ? 〈E0,goto … l st〉
     
    100100      ! v ← framesize globals st;
    101101      ! sp ← get_hwsp st;
    102         let newsp ≝ ?(*addr_add sp v*) in
     102      ! newsp ← addr_add sp v;
    103103      ! st ← set_hwsp newsp st;
    104104        ret ? 〈E0,goto … l st〉
     
    108108        ret ? 〈E0, goto … l st〉
    109109   ].
    110 qed.
    111110
    112111definition ertl_more_sem_params2: ∀globals. more_sem_params2 … (ertl_params globals) ≝
Note: See TracChangeset for help on using the changeset viewer.