Changeset 730 for src/CHANGES


Ignore:
Timestamp:
Apr 1, 2011, 12:03:31 PM (9 years ago)
Author:
campbell
Message:

A few deviations from the prototype / CompCert? that I can think of offhand.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/CHANGES

    r723 r730  
    1616  Added a dependent type for the invariant that a LIN function body does not
    1717  start with a label, and is not empty.
     18
     1901/04/2011:
     20  In retrospect:
     21
     22  The Clight semantics are based on CompCert 1.6 rather than the prototype's;
     23  this also affects some of the common files.
     24
     25    The identifiers are Words so that we can use BitVectorTries for maps.
     26    Similarly, integers are based on BitVectors rather than Coq-style binary
     27    integers + range proof.
     28
     29  8051 memory spaces are present, but are not (yet?) in the prototype.
     30
     31  Dependent types are used to fix the number of arguments for addressing modes
     32  in RTLabs.
Note: See TracChangeset for help on using the changeset viewer.