Changeset 730 for src

Timestamp:

Apr 1, 2011, 12:03:31 PM (10 years ago)

Author:

campbell

Message:

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

File:

• src/CHANGES (modified) (1 diff)

src/CHANGES

@@ -16 +16 @@
   Added a dependent type for the invariant that a LIN function body does not
   start with a label, and is not empty.
+
+01/04/2011:
+  In retrospect:
+
+  The Clight semantics are based on CompCert 1.6 rather than the prototype's;
+  this also affects some of the common files.
+
+    The identifiers are Words so that we can use BitVectorTries for maps.
+    Similarly, integers are based on BitVectors rather than Coq-style binary
+    integers + range proof.
+
+  8051 memory spaces are present, but are not (yet?) in the prototype.
+
+  Dependent types are used to fix the number of arguments for addressing modes
+  in RTLabs.