Merge of the newmem and newextcalls branches:

- Revised memory model with concrete representation of ints & floats,
  and per-byte access permissions
- Revised Globalenvs implementation
- Matching changes in all languages and proofs.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1282 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 11 insertions, 4 deletions

diff --git a/lib/Integers.v b/lib/Integers.v
index fb6eee23..b443d543 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -2670,15 +2670,15 @@ Qed.
 
 End Make.
 
-(** * Specialization to 32-bit integers. *)
+(** * Specialization to 32-bit integers and to bytes. *)
 
-Module IntWordsize.
+Module Wordsize_32.
   Definition wordsize := 32%nat.
   Remark wordsize_not_zero: wordsize <> 0%nat.
   Proof. unfold wordsize; congruence. Qed.
-End IntWordsize.
+End Wordsize_32.
 
-Module Int := Make(IntWordsize).
+Module Int := Make(Wordsize_32).
 
 Notation int := Int.int.
 
@@ -2688,5 +2688,12 @@ Proof.
   exists (two_p (32-5)); reflexivity. 
 Qed.
 
+Module Wordsize_8.
+  Definition wordsize := 8%nat.
+  Remark wordsize_not_zero: wordsize <> 0%nat.
+  Proof. unfold wordsize; congruence. Qed.
+End Wordsize_8.
 
+Module Byte := Integers.Make(Wordsize_8).
 
+Notation byte := Byte.int.