diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-16 18:01:25 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-16 18:01:25 +0100 |
| commit | fb02f9116621a0bcb9bb2c334ad782fee5887d0e (patch) | |
| tree | bce5373f7b3e1c88c4ca69b83da7f420840a5cba /mppa_k1c/Asmblockdeps.v | |
| parent | 8155320553564674b7481b325c33845439b46b95 (diff) | |
| download | compcert-kvx-fb02f9116621a0bcb9bb2c334ad782fee5887d0e.tar.gz compcert-kvx-fb02f9116621a0bcb9bb2c334ad782fee5887d0e.zip | |
partial norw
Diffstat (limited to 'mppa_k1c/Asmblockdeps.v')
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 499b0d66..0694c22f 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1302,6 +1302,7 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring := | Pandw => "Pandw" | Pnandw => "Pnandw" | Porw => "Porw" + | Pnorw => "Pnorw" | Pxorw => "Pxorw" | Psraw => "Psraw" | Psrlw => "Psrlw" @@ -1330,6 +1331,7 @@ Definition string_of_name_rri32 (n: arith_name_rri32): pstring := | Pandiw => "Pandiw" | Pnandiw => "Pnandiw" | Poriw => "Poriw" + | Pnoriw => "Pnoriw" | Pxoriw => "Pxoriw" | Psraiw => "Psraiw" | Psrliw => "Psrliw" |