diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-29 10:29:00 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-29 10:29:00 +0200 |
| commit | cd3642815d4260a9e7868fce3fb6a4a8a8ea8746 (patch) | |
| tree | 668ebaa8c884ae4bbf75186f3c1788555ddf535f /mppa_k1c/Asmblockdeps.v | |
| parent | 28312ed4869e3f63b0a113095d3344c0055ee2c5 (diff) | |
| download | compcert-kvx-cd3642815d4260a9e7868fce3fb6a4a8a8ea8746.tar.gz compcert-kvx-cd3642815d4260a9e7868fce3fb6a4a8a8ea8746.zip | |
Srsd / Srsw
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 8fccdd99..ff625bdd 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1287,6 +1287,7 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring := | Pornw => "Pornw" | Psraw => "Psraw" | Psrlw => "Psrlw" + | Psrxw => "Psrxw" | Psllw => "Psllw" | Paddl => "Paddl" | Psubl => "Psubl" @@ -1301,6 +1302,7 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring := | Pmull => "Pmull" | Pslll => "Pslll" | Psrll => "Psrll" + | Psrxl => "Psrxl" | Psral => "Psral" | Pfaddd => "Pfaddd" | Pfaddw => "Pfaddw" @@ -1325,11 +1327,13 @@ Definition string_of_name_rri32 (n: arith_name_rri32): pstring := | Porniw => "Porniw" | Psraiw => "Psraiw" | Psrliw => "Psrliw" + | Psrxiw => "Psrxiw" | Pslliw => "Pslliw" | Proriw => "Proriw" | Psllil => "Psllil" | Psrlil => "Psrlil" | Psrail => "Psrail" + | Psrxil => "Psrxil" end. Definition string_of_name_rri64 (n: arith_name_rri64): pstring := |