aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/Asmgen.v
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2018-04-10 13:51:50 +0200
committerCyril SIX <cyril.six@kalray.eu>2018-04-10 13:51:50 +0200
commit9862e89118492e6ab530b2e2992161dd4eb52d0a (patch)
tree2657be1ff60d44b78e5d65dd238ab867d7e4cc46 /mppa_k1c/Asmgen.v
parent5541fb2f156aa314e26cac65546458e47ba03264 (diff)
downloadcompcert-kvx-9862e89118492e6ab530b2e2992161dd4eb52d0a.tar.gz
compcert-kvx-9862e89118492e6ab530b2e2992161dd4eb52d0a.zip
MPPA - Onegl + Pnegl
Diffstat (limited to 'mppa_k1c/Asmgen.v')
-rw-r--r--mppa_k1c/Asmgen.v6
1 files changed, 3 insertions, 3 deletions
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v
index 4fed544f..1113bd4f 100644
--- a/mppa_k1c/Asmgen.v
+++ b/mppa_k1c/Asmgen.v
@@ -345,10 +345,10 @@ Definition transl_op
| Oaddlimm n, a1 :: nil =>
do rd <- ireg_of res; do rs <- ireg_of a1;
OK (addimm64 rd rs n k)
-(*| Onegl, a1 :: nil =>
+ | Onegl, a1 :: nil =>
do rd <- ireg_of res; do rs <- ireg_of a1;
- OK (Psubl rd GPR0 rs :: k)
- | Osubl, a1 :: a2 :: nil =>
+ OK (Pnegl rd rs :: k)
+(*| Osubl, a1 :: a2 :: nil =>
do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
OK (Psubl rd rs1 rs2 :: k)
| Omull, a1 :: a2 :: nil =>