From c7ffca253cf1767ae1416160e1a50bb5450c339f Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 4 Jul 2020 12:08:34 +0100 Subject: Remove mulhs and mulhu --- src/translation/HTLgen.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 4cde0c8..9a82aa8 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -324,8 +324,8 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := | Op.Osub, r1::r2::nil => ret (bop Vsub r1 r2) | Op.Omul, r1::r2::nil => ret (bop Vmul r1 r2) | Op.Omulimm n, r::nil => ret (boplit Vmul r n) - | Op.Omulhs, r1::r2::nil => ret (bop Vmul r1 r2) - | Op.Omulhu, r1::r2::nil => ret (bop Vmul r1 r2) + | Op.Omulhs, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mulhs") + | Op.Omulhu, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mulhu") | Op.Odiv, r1::r2::nil => ret (bop Vdiv r1 r2) | Op.Odivu, r1::r2::nil => ret (bop Vdivu r1 r2) | Op.Omod, r1::r2::nil => ret (bop Vmod r1 r2) -- cgit