diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-05 06:03:21 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-05 06:03:21 +0200 |
| commit | 53b6eb437c7988b44e881c7b7a9df2e735ded0ea (patch) | |
| tree | ffe451f96a6942088356246e8530fd0d9160cb7e /mppa_k1c/Asm.v | |
| parent | b27d386185527d1ee9d0bb77ebe3bacffc2bf05a (diff) | |
| download | compcert-kvx-53b6eb437c7988b44e881c7b7a9df2e735ded0ea.tar.gz compcert-kvx-53b6eb437c7988b44e881c7b7a9df2e735ded0ea.zip | |
select cmpu
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 2dc62e11..b323a67c 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -215,6 +215,7 @@ Inductive instruction : Type := | Pornil (rd rs: ireg) (imm: int64) (**r orn long *)
| Pmaddil (rd rs: ireg) (imm: int64) (**r multiply add imm long *)
| Pcmove (bt: btest) (rcond rd rs : ireg) (** conditional move *)
+ | Pcmoveu (bt: btest) (rcond rd rs : ireg) (** conditional move, unsigned semantics *)
.
(** Correspondance between Asmblock and Asm *)
@@ -363,6 +364,7 @@ Definition basic_to_instruction (b: basic) := | PArithARRR Asmblock.Pmaddw rd rs1 rs2 => Pmaddw rd rs1 rs2
| PArithARRR Asmblock.Pmaddl rd rs1 rs2 => Pmaddl rd rs1 rs2
| PArithARRR (Asmblock.Pcmove cond) rd rs1 rs2=> Pcmove cond rd rs1 rs2
+ | PArithARRR (Asmblock.Pcmoveu cond) rd rs1 rs2=> Pcmoveu cond rd rs1 rs2
(** ARRI32 *)
| PArithARRI32 Asmblock.Pmaddiw rd rs1 imm => Pmaddiw rd rs1 imm
|