diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-04 21:16:40 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-04 21:16:40 +0200 |
| commit | ac366a59308ae85a0cbfefb8b9be79763d5c5f91 (patch) | |
| tree | b533ea1790cf2b169c98e6af707b7e98b39869ac /mppa_k1c/Asmblockdeps.v | |
| parent | ed95a6a6fbdd915e361e696d4bf72e5a545b965e (diff) | |
| download | compcert-kvx-ac366a59308ae85a0cbfefb8b9be79763d5c5f91.tar.gz compcert-kvx-ac366a59308ae85a0cbfefb8b9be79763d5c5f91.zip | |
added immediate cmove
Diffstat (limited to 'mppa_k1c/Asmblockdeps.v')
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 616ec6db..265c4e84 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1515,11 +1515,15 @@ Definition string_of_name_arr (n: arith_name_arr): pstring := Definition string_of_name_arri32 (n: arith_name_arri32): pstring := match n with | Pmaddiw => "Pmaddw" + | Pcmoveiw _ => "Pcmoveiw" + | Pcmoveuiw _ => "Pcmoveuiw" end. Definition string_of_name_arri64 (n: arith_name_arri64): pstring := match n with | Pmaddil => "Pmaddl" + | Pcmoveil _ => "Pcmoveil" + | Pcmoveuil _ => "Pcmoveuil" end. Definition string_of_arith (op: arith_op): pstring := |