From 3750a2ad965b4959f6535aeeb9075dbd1a7c0527 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 26 Mar 2019 22:44:31 +0100 Subject: selectl generation --- mppa_k1c/Asmblockgen.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'mppa_k1c/Asmblockgen.v') diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 6e025381..cf0b2a0a 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 BTwnez r0 rS r1 ::i k) + OK (Pcmove BTdnez r0 rS r1 ::i k) | _, _ => Error(msg "Asmgenblock.transl_op") -- cgit