diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-03 21:59:22 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-03 21:59:22 +0200 |
| commit | 4518486a771055e633aa050141d9721353d542d7 (patch) | |
| tree | 0916e82f7229068dd492c9552c248d9d94137920 /mppa_k1c/Asmblockgen.v | |
| parent | 104681e5db184659a36762e0776cef133d70455b (diff) | |
| download | compcert-kvx-4518486a771055e633aa050141d9721353d542d7.tar.gz compcert-kvx-4518486a771055e633aa050141d9721353d542d7.zip | |
ternary ops in AES and TEA
Diffstat (limited to 'mppa_k1c/Asmblockgen.v')
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 6315192c..a7e3c8ef 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -741,7 +741,7 @@ Definition transl_op do r0 <- ireg_of a0; do r1 <- ireg_of a1; do rS <- ireg_of aS; - OK (Pcmove BTdnez r0 rS r1 ::i k) + OK (Pcmove BTwnez r0 rS r1 ::i k) | _, _ => Error(msg "Asmgenblock.transl_op") |