diff options
author | Michael Schmidt <github@mschmidt.me> | 2016-09-15 13:02:33 +0200 |
---|---|---|
committer | Michael Schmidt <github@mschmidt.me> | 2016-09-15 13:03:01 +0200 |
commit | 4cbdaa1a71c91b33136144b76ac2b7d6906688bc (patch) | |
tree | 251701d22cd364e144e7ce744d0d2940b5ce73f0 | |
parent | 6f2b5713f8e378e6e074f35a537e86a497c64e35 (diff) | |
download | compcert-4cbdaa1a71c91b33136144b76ac2b7d6906688bc.tar.gz compcert-4cbdaa1a71c91b33136144b76ac2b7d6906688bc.zip |
improve fixup code (bug 19792)
-rw-r--r-- | arm/TargetPrinter.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 609d2475..6d194369 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -382,8 +382,10 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = end | (fr, Single, sr) :: act -> let n = fixup_incoming oc act in + if (2*fr) = sr then n else begin fprintf oc " vmov.f32 s%d, s%d\n" (2*fr) sr; 1 + n + end let fixup_arguments oc dir sg = if sg.sig_cc.cc_vararg then |