diff options
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. |