Merge of the newmem branch:

- Revised memory model with Max and Cur permissions, but without bounds
- Constant propagation of 'const' globals
- Function inlining at RTL level
- (Unprovable) elimination of unreferenced static definitions


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

1 files changed, 8 insertions, 0 deletions

diff --git a/driver/Interp.ml b/driver/Interp.ml
index 62f3093b..a74d4d8e 100644
--- a/driver/Interp.ml
+++ b/driver/Interp.ml
@@ -145,6 +145,12 @@ let mem_of_state = function
 
 (* Comparing memory states *)
 
+let compare_mem m1 m2 =
+  Pervasives.compare (m1.Mem.nextblock, m1.Mem.mem_contents)
+                     (m2.Mem.nextblock, m1.Mem.mem_contents)
+(* FIXME: should permissions be taken into account? *)
+
+(*
 let rec compare_Z_range lo hi f =
   if coq_Zcompare lo hi = Lt then begin
     let c = f lo in if c <> 0 then c else compare_Z_range (coq_Zsucc lo) hi f
@@ -154,6 +160,7 @@ let compare_mem m1 m2 =
   if m1 == m2 then 0 else
   let c = compare m1.Mem.nextblock m2.Mem.nextblock in if c <> 0 then c else
   compare_Z_range Z0 m1.Mem.nextblock (fun b ->
+
     let ((lo, hi) as bnds) = m1.Mem.bounds b in
     let c = compare bnds (m2.Mem.bounds b) in if c <> 0 then c else
     let contents1 = m1.Mem.mem_contents b and contents2 = m2.Mem.mem_contents b in
@@ -163,6 +170,7 @@ let compare_mem m1 m2 =
     let access1 = m1.Mem.mem_access b and access2 = m2.Mem.mem_access b in
     if access1 == access2 then 0 else
     compare_Z_range lo hi (fun ofs -> compare (access1 ofs) (access2 ofs)))
+*)
 
 (* Comparing continuations *)