Changeset 1213 for src/common/AST.ma


Ignore:
Timestamp:
Sep 15, 2011, 2:01:56 PM (9 years ago)
Author:
sacerdot
Message:

1) New values (joint/BEValues.ma) and memory model for the back-ends

(joint/BEMem.ma) where all values are Byte-valued.

2) Improved joint semantics for the back-end languages based on the new

memory model (work in progress).

3) SmallStepExec? made more general to accomodate states with an arbitrary

memory inside.

4) New files common/Pointers.ma and common/GenMem.ma shared between the

front-end and the back-end. GenMem?.ma, at the moment, is not used in Mem.ma
(cut&paste code).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r1139 r1213  
    8484try ( @Ptrue // )
    8585@Pfalse % #E destruct
     86qed.
     87
     88lemma reflexive_eq_region: ∀r. eq_region r r = true.
     89 * //
    8690qed.
    8791
Note: See TracChangeset for help on using the changeset viewer.