aboutsummaryrefslogtreecommitdiffstats
path: root/arm/extractionMachdep.v
diff options
context:
space:
mode:
authorxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2009-11-03 08:43:54 +0000
committerxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2009-11-03 08:43:54 +0000
commit0486654fac91947fec93d18a0738dd7aa10bcf96 (patch)
tree4f6b954a2dcc74df25c05bc4c15f0f317aa2d780 /arm/extractionMachdep.v
parente47dcb416c68da4e559d70e633276f7227659740 (diff)
downloadcompcert-kvx-0486654fac91947fec93d18a0738dd7aa10bcf96.tar.gz
compcert-kvx-0486654fac91947fec93d18a0738dd7aa10bcf96.zip
PowerPC/EABI port: preliminary support for #pragma section and
#pragma use_section. Some clean-ups in Cil2Csyntax. Separate mach-dep parts of extraction/extraction.v into <arch>/extractionMachdep.v git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1167 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'arm/extractionMachdep.v')
-rw-r--r--arm/extractionMachdep.v18
1 files changed, 18 insertions, 0 deletions
diff --git a/arm/extractionMachdep.v b/arm/extractionMachdep.v
new file mode 100644
index 00000000..f6e17bab
--- /dev/null
+++ b/arm/extractionMachdep.v
@@ -0,0 +1,18 @@
+(* *********************************************************************)
+(* *)
+(* 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. *)
+(* *)
+(* *********************************************************************)
+
+(* Additional extraction directives specific to the ARM port *)
+
+(* Suppression of stupidly big equality functions *)
+Extract Constant Asm.ireg_eq => "fun (x: ireg) (y: ireg) -> x = y".
+Extract Constant Asm.freg_eq => "fun (x: freg) (y: freg) -> x = y".
+Extract Constant Asm.preg_eq => "fun (x: preg) (y: preg) -> x = y".