diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-07-27 07:35:49 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-07-27 07:35:49 +0000 |
| commit | f4e106d4fc1cce484678b5cdd86ab57d7a43076a (patch) | |
| tree | 3de9bddc63b80fb1b695bbdb8fa5bd6aa893a13a /arm/Archi.v | |
| parent | 04ff02a9f4bc4f766a450e5463729102ee26882e (diff) | |
ARM port: add support for Thumb2. To be tested.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2549 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'arm/Archi.v')
| -rw-r--r-- | arm/Archi.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/arm/Archi.v b/arm/Archi.v index 1306459..00d9895 100644 --- a/arm/Archi.v +++ b/arm/Archi.v @@ -47,5 +47,9 @@ Global Opaque big_endian default_pl_64 choose_binop_pl_64 default_pl_32 choose_binop_pl_32. +(** Which ABI to use: either the standard ARM EABI with floats passed + in integer registers, or the "hardfloat" variant of the EABI + that uses FP registers instead. *) + Inductive abi_kind := Softfloat | Hardfloat. Parameter abi: abi_kind. |