- Added alignment constraints to memory loads and stores.

- In Cminor and below, removed pointer validity check in semantics of 
  comparisons, so that evaluation of expressions is independent of
  memory state.
- In Cminor and below, removed "alloc" instruction.
- Cleaned up commented-away parts.


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

1 files changed, 12 insertions, 1 deletions

diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v
index ce19f68..1aa536a 100644
--- a/cfrontend/Csharpminor.v
+++ b/cfrontend/Csharpminor.v
@@ -181,7 +181,18 @@ Definition eval_constant (cst: constant) : option val :=
   end.
 
 Definition eval_unop := Cminor.eval_unop.
-Definition eval_binop := Cminor.eval_binop.
+
+Definition eval_binop (op: binary_operation)
+                      (arg1 arg2: val) (m: mem): option val :=
+  match op, arg1, arg2 with
+  | Cminor.Ocmp c, Vptr b1 n1, Vptr b2 n2 =>
+      if valid_pointer m b1 (Int.signed n1)
+      && valid_pointer m b2 (Int.signed n2)
+      then Cminor.eval_binop op arg1 arg2
+      else None
+  | _, _, _ =>
+      Cminor.eval_binop op arg1 arg2
+  end.
 
 (** Allocation of local variables at function entry.  Each variable is
   bound to the reference to a fresh block of the appropriate size. *)