aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-01-17 20:20:40 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-01-17 20:20:40 +0100
commitf4c2e3fb9c012685c1ecd4ee24ff838619238fe2 (patch)
tree2d6c491ebdab600588fcc69131ad7ba4de867094 /mppa_k1c
parentf9a0dd579dc72b09c4ebb036df0b59891412163d (diff)
parentc953ce47894f58f3fc88c0f93e6bcac9ad0301ac (diff)
downloadcompcert-kvx-f4c2e3fb9c012685c1ecd4ee24ff838619238fe2.tar.gz
compcert-kvx-f4c2e3fb9c012685c1ecd4ee24ff838619238fe2.zip
Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
Diffstat (limited to 'mppa_k1c')
-rw-r--r--mppa_k1c/Asmexpand.ml1
-rw-r--r--mppa_k1c/PostpassSchedulingOracle.ml4
2 files changed, 3 insertions, 2 deletions
diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml
index 0252ce85..265de410 100644
--- a/mppa_k1c/Asmexpand.ml
+++ b/mppa_k1c/Asmexpand.ml
@@ -350,6 +350,7 @@ match !vararg_start_ofs with
invalid_arg "Fatal error: va_start used in non-vararg function"
| Some ofs ->
expand_addptrofs Asmblock.GPR32 Asmblock.GPR12 (Ptrofs.repr ofs);
+ emit Psemi;
expand_storeind_ptr Asmblock.GPR32 r Ptrofs.zero
(* Auxiliary for 64-bit integer arithmetic built-ins. They expand to
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index 4291316a..19d4d962 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -356,9 +356,9 @@ let ab_inst_to_real = function
| "Psllw" | "Pslliw" -> Sllw
| "Pslll" | "Psllil" -> Slld
| "Pxorw" | "Pxoriw" -> Xorw
- | "Pxord" | "Pxoril" -> Xord
+ | "Pxorl" | "Pxoril" -> Xord
| "Pmake" | "Pmakel" | "Ploadsymbol" -> Make
- | "Pnop" | "Pcvtwl2w" -> Nop
+ | "Pnop" | "Pcvtw2l" -> Nop
| "Plb" -> Lbs
| "Plbu" -> Lbz