- 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, 0 insertions, 4 deletions

diff --git a/backend/Allocation.v b/backend/Allocation.v
index 3a5960b..2389a33 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -101,8 +101,6 @@ Definition transfer
            (reg_sum_live ros (reg_dead res after))
       | Itailcall sig ros args =>
 	  reg_list_live args (reg_sum_live ros Regset.empty)
-      | Ialloc arg res s =>
-          reg_live arg (reg_dead res after)
       | Icond cond args ifso ifnot =>
           reg_list_live args after
       | Ireturn optarg =>
@@ -167,8 +165,6 @@ Definition transf_instr
                 (assign res) s
   | Itailcall sig ros args =>
       Ltailcall sig (sum_left_map assign ros) (List.map assign args)
-  | Ialloc arg res s =>
-      Lalloc (assign arg) (assign res) s
   | Icond cond args ifso ifnot =>
       Lcond cond (List.map assign args) ifso ifnot
   | Ireturn optarg =>