diff options
| author | Nadesh Ramanathan <nadeshramanathan88@gmail.com> | 2020-07-04 13:53:46 +0100 |
|---|---|---|
| committer | Nadesh Ramanathan <nadeshramanathan88@gmail.com> | 2020-07-04 13:53:46 +0100 |
| commit | 985f425eb77478a55e9cc8359229798128ff9840 (patch) | |
| tree | 59cd9affa17355d8b747009cb2c85cb385e8c9ef | |
| parent | dd896636c7a1a2a8ad45f07bf081b8f6374f9fd8 (diff) | |
| parent | 6613005bf68310eae57f35026ae72a06c5f4cfe5 (diff) | |
| download | vericert-kvx-985f425eb77478a55e9cc8359229798128ff9840.tar.gz vericert-kvx-985f425eb77478a55e9cc8359229798128ff9840.zip | |
Merge branch 'dev-nadesh-proven' of https://github.com/ymherklotz/coqup into dev-nadesh-proven
| -rw-r--r-- | src/translation/HTLgen.v | 4 |
1 files 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) |