diff options
Diffstat (limited to 'powerpc/Archi.v')
| -rw-r--r-- | powerpc/Archi.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/powerpc/Archi.v b/powerpc/Archi.v index ab348c14..10f38391 100644 --- a/powerpc/Archi.v +++ b/powerpc/Archi.v @@ -30,6 +30,10 @@ Definition align_float64 := 8%Z. (** Can we use the 64-bit extensions to the PowerPC architecture? *) Parameter ppc64 : bool. +(** 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. Lemma splitlong_ptr32: splitlong = true -> ptr64 = false. |