- Timestamp:
- Apr 1, 2011, 12:03:31 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/CHANGES
r723 r730 16 16 Added a dependent type for the invariant that a LIN function body does not 17 17 start with a label, and is not empty. 18 19 01/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.