diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-02-14 18:51:52 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-02-14 18:51:52 +0100 |
| commit | 1ef9e303d7bd896b94afcc875136d8f3e94243cb (patch) | |
| tree | af2da3d2fdbc0be85d207bf20111162bcf0a4f56 /kvx/Asmblockdeps.v | |
| parent | 882f1a1875089298937abf4ef854b221cab4eb8e (diff) | |
| parent | 2867dee21f6fb696db554679d8535306c7a9d4ea (diff) | |
| download | compcert-kvx-1ef9e303d7bd896b94afcc875136d8f3e94243cb.tar.gz compcert-kvx-1ef9e303d7bd896b94afcc875136d8f3e94243cb.zip | |
Merge remote-tracking branch 'origin/kvx-bits' into kvx_fp_division
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 ac0b359e..78a766ee 100644 --- a/kvx/Asmblockdeps.v +++ b/kvx/Asmblockdeps.v @@ -1613,6 +1613,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 := @@ -1640,6 +1642,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 := @@ -1658,6 +1661,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 := |