summaryrefslogtreecommitdiff
path: root/powerpc
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-01-02 15:59:11 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2014-01-02 15:59:11 +0000
commit29e0c9b2c99a437fc9dfab66e1abdd546a5308d6 (patch)
tree2c3e924125d9b91e5e9b57b87c80f5b5ce9c6710 /powerpc
parentc71e155dbbf34fa17d14e8eee50a019c8ccfd6f5 (diff)
Updated ARM backend wrt new static analyses and optimizations.
NeedOp, Deadcode: must have distinct needs per argument of an operator. This change remains to be propagated to IA32 and PPC. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2399 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc')
-rw-r--r--powerpc/ValueAOp.v12
1 files changed, 12 insertions, 0 deletions
diff --git a/powerpc/ValueAOp.v b/powerpc/ValueAOp.v
index 12cb8e4..3789953 100644
--- a/powerpc/ValueAOp.v
+++ b/powerpc/ValueAOp.v
@@ -1,3 +1,15 @@
+(* *********************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* Xavier Leroy, INRIA Paris-Rocquencourt *)
+(* *)
+(* Copyright Institut National de Recherche en Informatique et en *)
+(* Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the INRIA Non-Commercial License Agreement. *)
+(* *)
+(* *********************************************************************)
+
Require Import Coqlib.
Require Import AST.
Require Import Integers.