diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-02-14 15:48:43 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-02-14 15:48:43 +0100 |
| commit | f6686d81092ccaaf3a22b4e34aecc7c5895b08ba (patch) | |
| tree | 9d61868c2ad5e0ed20329512d9508280da1e4c70 /kvx/Asmblockdeps.v | |
| parent | b7aea86a0c6ace274e585fddfd0d88d13528cc90 (diff) | |
| download | compcert-kvx-f6686d81092ccaaf3a22b4e34aecc7c5895b08ba.tar.gz compcert-kvx-f6686d81092ccaaf3a22b4e34aecc7c5895b08ba.zip | |
begin adding abdw abdd
Diffstat (limited to 'kvx/Asmblockdeps.v')
| -rw-r--r-- | kvx/Asmblockdeps.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kvx/Asmblockdeps.v b/kvx/Asmblockdeps.v index a9786e0a..b1895ee6 100644 --- a/kvx/Asmblockdeps.v +++ b/kvx/Asmblockdeps.v @@ -1609,6 +1609,8 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring := | Pfminw => "Pfminw" | Pfmaxd => "Pfmaxd" | Pfmaxw => "Pfmaxw" + | Pabdw => "Pabdw" + | Pabdl => "Pabdl" end. Definition string_of_name_rri32 (n: arith_name_rri32): pstring := @@ -1636,6 +1638,7 @@ Definition string_of_name_rri32 (n: arith_name_rri32): pstring := | Psrlil => "Psrlil" | Psrail => "Psrail" | Psrxil => "Psrxil" + | Pabdiw => "Pabdiw" end. Definition string_of_name_rri64 (n: arith_name_rri64): pstring := @@ -1654,6 +1657,7 @@ Definition string_of_name_rri64 (n: arith_name_rri64): pstring := | Pnxoril => "Pnxoril" | Pandnil => "Pandnil" | Pornil => "Pornil" + | Pabdil => "Pabdil" end. Definition string_of_name_arrr (n: arith_name_arrr): pstring := |