From 680ab18c29b5f72483780146d83e01c8ab498fb9 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 25 Mar 2019 10:45:26 +0100 Subject: progress on cmove --- mppa_k1c/Asmblockdeps.v | 1 + 1 file changed, 1 insertion(+) (limited to 'mppa_k1c/Asmblockdeps.v') diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index ad96ae87..7ea4c9ee 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1433,6 +1433,7 @@ Definition string_of_name_arrr (n: arith_name_arrr): pstring := match n with | Pmaddw => "Pmaddw" | Pmaddl => "Pmaddl" + | Pcmove _ => "Pcmove" end. Definition string_of_name_arri32 (n: arith_name_arri32): pstring := -- cgit From 53b6eb437c7988b44e881c7b7a9df2e735ded0ea Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 5 Apr 2019 06:03:21 +0200 Subject: select cmpu --- mppa_k1c/Asmblockdeps.v | 1 + 1 file changed, 1 insertion(+) (limited to 'mppa_k1c/Asmblockdeps.v') diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index d8ca465e..96547342 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1446,6 +1446,7 @@ Definition string_of_name_arrr (n: arith_name_arrr): pstring := | Pmaddw => "Pmaddw" | Pmaddl => "Pmaddl" | Pcmove _ => "Pcmove" + | Pcmoveu _ => "Pcmoveu" end. Definition string_of_name_arri32 (n: arith_name_arri32): pstring := -- cgit