From f401437a97b09726d029e3a1b65143f34baaea70 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 24 Feb 2013 09:40:25 +0000
Subject: Updated ARM and PowerPC ports with new handling of __builtin_annot.
 ARM: add support for builtin_volatile_{read,write}_global, after all.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2127 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 arm/ConstpropOp.vp | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'arm/ConstpropOp.vp')

diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp
index a9cbad5d..7e3217ee 100644
--- a/arm/ConstpropOp.vp
+++ b/arm/ConstpropOp.vp
@@ -335,8 +335,4 @@ Nondetfunction addr_strength_reduction
       (addr, args)
   end.
 
-Definition builtin_strength_reduction
-               (ef: external_function) (args: list reg) (vl: list approx) :=
-  (ef, args).
-
 End STRENGTH_REDUCTION.
-- 
cgit