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 --- powerpc/Constprop.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'powerpc/Constprop.v') diff --git a/powerpc/Constprop.v b/powerpc/Constprop.v index 75fb1486..6ec27a3f 100644 --- a/powerpc/Constprop.v +++ b/powerpc/Constprop.v @@ -654,8 +654,10 @@ Definition transfer (f: function) (pc: node) (before: D.t) := D.set res Unknown before | Itailcall sig ros args => before +(* | Ialloc arg res s => D.set res Unknown before +*) | Icond cond args ifso ifnot => before | Ireturn optarg => @@ -1045,8 +1047,6 @@ Definition transf_instr (approx: D.t) (instr: instruction) := Icall sig (transf_ros approx ros) args res s | Itailcall sig ros args => Itailcall sig (transf_ros approx ros) args - | Ialloc arg res s => - Ialloc arg res s | Icond cond args s1 s2 => match eval_static_condition cond (approx_regs args approx) with | Some b => -- cgit