diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-02-27 10:15:40 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2020-03-02 10:30:15 +0100 |
| commit | 35ba7f373963d8a1f0094abd457809d1e3c3cdb4 (patch) | |
| tree | c5b61f1716c0d70df46e1de6e4c9499c080cd5da /powerpc | |
| parent | 9190ca38b3ae098186421a7cc21a087666a6a677 (diff) | |
| download | compcert-35ba7f373963d8a1f0094abd457809d1e3c3cdb4.tar.gz compcert-35ba7f373963d8a1f0094abd457809d1e3c3cdb4.zip | |
Documentation comment for single_passed_as_single
Diffstat (limited to 'powerpc')
| -rw-r--r-- | powerpc/Archi.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/powerpc/Archi.v b/powerpc/Archi.v index 88fff302..10f38391 100644 --- a/powerpc/Archi.v +++ b/powerpc/Archi.v @@ -30,7 +30,8 @@ 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 *) +(** Should single-precision FP arguments passed on stack be passed + as singles or use double FP format. *) Parameter single_passed_as_single : bool. Definition splitlong := negb ppc64. |