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

1 files changed, 24 insertions, 0 deletions

diff --git a/powerpc/extractionMachdep.v b/powerpc/extractionMachdep.v
new file mode 100644
index 0000000..46c40ca
--- /dev/null
+++ b/powerpc/extractionMachdep.v
@@ -0,0 +1,24 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 PowerPC port *)
+
+(* Asm *)
+Extract Constant Asm.low_half => "fun _ -> assert false".
+Extract Constant Asm.high_half => "fun _ -> assert false".
+Extract Constant Asm.symbol_is_small_data => "CPragmas.atom_is_small_data".
+Extract Constant Asm.small_data_area_offset => "fun _ _ _ -> assert false".
+
+(* 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".