diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-02-27 10:10:23 +0100 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2020-03-02 10:30:15 +0100 |
commit | 9190ca38b3ae098186421a7cc21a087666a6a677 (patch) | |
tree | 2822d34169dfe7c323bcdeab6f32f3c776cd6710 /lib/IntvSets.v | |
parent | 78d76b65b417b2724cc54a7e5fc5d434d8fc57b5 (diff) | |
download | compcert-9190ca38b3ae098186421a7cc21a087666a6a677.tar.gz compcert-9190ca38b3ae098186421a7cc21a087666a6a677.zip |
In strict PPC ABI mode, pass single FP on stack in double FP format
The EABI and the SVR4 ABI state that single-precision FP arguments passed
on stack are passed as a 64-bit word, extended to double-precision.
This commit implements this behavior by using a stack slot of type Tany64.
Not only this ensures that the slot is of size and alignment 8 bytes,
but it also ensures that it is accessed by stfd and lfd instructions,
using single-extended-to-double format.
Diffstat (limited to 'lib/IntvSets.v')
0 files changed, 0 insertions, 0 deletions