- 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, 1 insertions, 3 deletions

diff --git a/backend/Bounds.v b/backend/Bounds.v
index e598245..d1ed28d 100644
--- a/backend/Bounds.v
+++ b/backend/Bounds.v
@@ -26,8 +26,7 @@ Require Import Conventions.
 (** The [bounds] record capture how many local and outgoing stack slots
   and callee-save registers are used by a function. *)
 
-(** We demand that all bounds are positive or null,
-  and moreover [bound_outgoing] is greater or equal to 6.
+(** We demand that all bounds are positive or null.
   These properties are used later to reason about the layout of
   the activation record. *)
 
@@ -104,7 +103,6 @@ Definition regs_of_instr (i: instruction) : list mreg :=
   | Lstore chunk addr args src => nil
   | Lcall sig ros => nil
   | Ltailcall sig ros => nil
-  | Lalloc => nil
   | Llabel lbl => nil
   | Lgoto lbl => nil
   | Lcond cond args lbl => nil