diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2019-03-18 16:14:13 +0100 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2019-03-18 16:14:13 +0100 |
commit | eec959218b8dc4e994ee843d7cbd1cf5a0cbcdcc (patch) | |
tree | c44bd4584a17cfa113bc66665e67caa6df820d50 /mppa_k1c/Asmblockdeps.v | |
parent | aa400a9eed939578917810d32ef4fcf79944729d (diff) | |
parent | 202050c6240a11c94cc8b6ab599022fee7bd2471 (diff) | |
download | compcert-kvx-eec959218b8dc4e994ee843d7cbd1cf5a0cbcdcc.tar.gz compcert-kvx-eec959218b8dc4e994ee843d7cbd1cf5a0cbcdcc.zip |
Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass
Diffstat (limited to 'mppa_k1c/Asmblockdeps.v')
-rw-r--r-- | mppa_k1c/Asmblockdeps.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index b77fa47d..a2d75b27 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1305,6 +1305,8 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring := | Pnorw => "Pnorw" | Pxorw => "Pxorw" | Pnxorw => "Pnxorw" + | Pandnw => "Pandnw" + | Pornw => "Pornw" | Psraw => "Psraw" | Psrlw => "Psrlw" | Psllw => "Psllw" @@ -1316,6 +1318,8 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring := | Pnorl => "Pnorl" | Pxorl => "Pxorl" | Pnxorl => "Pnxorl" + | Pandnl => "Pandnl" + | Pornl => "Pornl" | Pmull => "Pmull" | Pslll => "Pslll" | Psrll => "Psrll" @@ -1338,6 +1342,8 @@ Definition string_of_name_rri32 (n: arith_name_rri32): pstring := | Pnoriw => "Pnoriw" | Pxoriw => "Pxoriw" | Pnxoriw => "Pnxoriw" + | Pandniw => "Pandniw" + | Porniw => "Porniw" | Psraiw => "Psraiw" | Psrliw => "Psrliw" | Pslliw => "Pslliw" @@ -1357,6 +1363,8 @@ Definition string_of_name_rri64 (n: arith_name_rri64): pstring := | Pnoril => "Pnoril" | Pxoril => "Pxoril" | Pnxoril => "Pnxoril" + | Pandnil => "Pandnil" + | Pornil => "Pornil" end. Definition string_of_arith (op: arith_op): pstring := |