diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2020-02-24 19:59:43 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2020-03-02 10:30:15 +0100 |
| commit | e66be6e05b190c51b38d628884ef3e015ebf73fd (patch) | |
| tree | 4a2e85c65530596418981238e5672998d5ad0857 /powerpc/Archi.v | |
| parent | 5003b8d93c2a20821b776f7f74f5096a308a03cf (diff) | |
| download | compcert-kvx-e66be6e05b190c51b38d628884ef3e015ebf73fd.tar.gz compcert-kvx-e66be6e05b190c51b38d628884ef3e015ebf73fd.zip | |
Make single arg alignment depend on toolchain.
GCC does passes single arguments as singles on the stack but diab
and the eabi say single arguments should be passed as double on
the stack.
This commit changes the alignment of single arguments to 4 for
gcc based backends.
Diffstat (limited to 'powerpc/Archi.v')
| -rw-r--r-- | powerpc/Archi.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/powerpc/Archi.v b/powerpc/Archi.v index ab348c14..88fff302 100644 --- a/powerpc/Archi.v +++ b/powerpc/Archi.v @@ -30,6 +30,9 @@ Definition align_float64 := 8%Z. (** Can we use the 64-bit extensions to the PowerPC architecture? *) Parameter ppc64 : bool. +(** Should singles be passed as single or double *) +Parameter single_passed_as_single : bool. + Definition splitlong := negb ppc64. Lemma splitlong_ptr32: splitlong = true -> ptr64 = false. |