From bb9d14a3f95fc0e3c8cad10d8ea8e2b2738da7fc Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 11 Jan 2009 11:57:02 +0000 Subject: - 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 --- backend/Allocation.v | 4 ---- 1 file changed, 4 deletions(-) (limited to 'backend/Allocation.v') diff --git a/backend/Allocation.v b/backend/Allocation.v index 3a5960be..2389a331 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 => -- cgit