diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-07-23 13:14:02 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-07-23 13:14:02 +0000 |
| commit | 783288d052bbcf75e250dff5018443d109c6101c (patch) | |
| tree | c7254dde41f1bb1229cad9f49a0bfd4482293aba /arm/extractionMachdep.v | |
| parent | ae6f7b8d4cf30fbc2f56c3f2baa8f028fb7f9c10 (diff) | |
| download | compcert-kvx-783288d052bbcf75e250dff5018443d109c6101c.tar.gz compcert-kvx-783288d052bbcf75e250dff5018443d109c6101c.zip | |
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
Diffstat (limited to 'arm/extractionMachdep.v')
| -rw-r--r-- | arm/extractionMachdep.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/arm/extractionMachdep.v b/arm/extractionMachdep.v index f6e17bab..0c9b7056 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". |