From 0053b1aa1d26da5d1f995a603b127daf799c2da9 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 21 May 2012 16:26:30 +0000
Subject: Merge of the newmem branch: - Revised memory model with Max and Cur
 permissions, but without bounds - Constant propagation of 'const' globals -
 Function inlining at RTL level - (Unprovable) elimination of unreferenced
 static definitions

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 powerpc/Unusedglob1.ml | 61 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 61 insertions(+)
 create mode 100644 powerpc/Unusedglob1.ml

(limited to 'powerpc/Unusedglob1.ml')

diff --git a/powerpc/Unusedglob1.ml b/powerpc/Unusedglob1.ml
new file mode 100644
index 0000000..c16cd2f
--- /dev/null
+++ b/powerpc/Unusedglob1.ml
@@ -0,0 +1,61 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* Identifiers referenced from a PowerPC Asm instruction *)
+
+open Datatypes
+open AST
+open Asm
+
+let referenced_constant = function
+  | Cint n -> []
+  | Csymbol_low(s, ofs) -> [s]
+  | Csymbol_high(s, ofs) -> [s]
+  | Csymbol_sda(s, ofs) -> [s]
+
+let referenced_builtin ef =
+  match ef with
+  | EF_vload_global(chunk, id, ofs) -> [id]
+  | EF_vstore_global(chunk, id, ofs) -> [id]
+  | _ -> []
+
+let referenced_instr = function
+  | Pbl s -> [s]
+  | Pbs s -> [s]
+  | Paddi(_, _, c)
+  | Paddic(_, _, c)
+  | Paddis(_, _, c)
+  | Pandi_(_, _, c)
+  | Pandis_(_, _, c)
+  | Pcmplwi(_, c)
+  | Pcmpwi(_, c)
+  | Plbz(_, c, _)
+  | Plfd(_, c, _)
+  | Plfs(_, c, _)
+  | Plha(_, c, _)
+  | Plhz(_, c, _)
+  | Plwz(_, c, _)
+  | Pmulli(_, _, c)
+  | Pori(_, _, c)
+  | Poris(_, _, c)
+  | Pstb(_, c, _)
+  | Pstfd(_, c, _)
+  | Pstfs(_, c, _)
+  | Psth(_, c, _) 
+  | Pstw(_, c, _) 
+  | Psubfic(_, _, c)
+  | Pxori(_, _, c)
+  | Pxoris(_, _, c) -> referenced_constant c
+  | Pbuiltin(ef, _, _) -> referenced_builtin ef
+  | _ -> []
+
+let code_of_function f = f
-- 
cgit v1.2.3