From 783288d052bbcf75e250dff5018443d109c6101c Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 23 Jul 2014 13:14:02 +0000 Subject: Merge the various $(ARCH)/$(VARIANT)/xxx.v files into $(ARCH)/xxx.v. The only platform where we have two variants is ARM, and it's easier to share the callling convention code between the two than to maintain both variants separately. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2540 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/extractionMachdep.v | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'arm/extractionMachdep.v') diff --git a/arm/extractionMachdep.v b/arm/extractionMachdep.v index f6e17ba..0c9b705 100644 --- a/arm/extractionMachdep.v +++ b/arm/extractionMachdep.v @@ -16,3 +16,11 @@ 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". + +(* Choice of calling conventions *) +Extract Constant Archi.abi => + "begin match Configuration.variant with + | ""eabi"" -> Softfloat + | ""hardfloat"" -> Hardfloat + | _ -> assert false + end". -- cgit v1.2.3