diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-10 20:02:11 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-10 20:02:11 +0200 |
commit | 95b43cbcc4390d9058034b769ffa757c42d2a74f (patch) | |
tree | 66885177e24f366dfbd447a4ffc9fa644d92fa15 /mppa_k1c/Asmblockdeps.v | |
parent | 212b467687f0e3c0e3897b501cdc9e09a0d99233 (diff) | |
download | compcert-kvx-95b43cbcc4390d9058034b769ffa757c42d2a74f.tar.gz compcert-kvx-95b43cbcc4390d9058034b769ffa757c42d2a74f.zip |
new instructions at asm level
Diffstat (limited to 'mppa_k1c/Asmblockdeps.v')
-rw-r--r-- | mppa_k1c/Asmblockdeps.v | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index eb3900d5..82062fab 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1405,12 +1405,14 @@ Definition string_of_name_rf64 (n: arith_name_rf64): pstring := Definition string_of_name_rrr (n: arith_name_rrr): pstring := match n with - Pcompw _ => "Pcompw" + | Pcompw _ => "Pcompw" | Pcompl _ => "Pcompl" | Pfcompw _ => "Pfcompw" | Pfcompl _ => "Pfcompl" | Paddw => "Paddw" + | Paddxw _ => "Paddxw" | Psubw => "Psubw" + | Psubxw _ => "Psubxw" | Pmulw => "Pmulw" | Pandw => "Pandw" | Pnandw => "Pnandw" @@ -1425,7 +1427,9 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring := | Psrxw => "Psrxw" | Psllw => "Psllw" | Paddl => "Paddl" + | Paddxl _ => "Paddxl" | Psubl => "Psubl" + | Psubxl _ => "Psubxl" | Pandl => "Pandl" | Pnandl => "Pnandl" | Porl => "Porl" @@ -1451,6 +1455,9 @@ Definition string_of_name_rri32 (n: arith_name_rri32): pstring := match n with Pcompiw _ => "Pcompiw" | Paddiw => "Paddiw" + | Psubiw => "Psubiw" + | Paddxiw _ => "Paddxiw" + | Psubxiw _ => "Psubxiw" | Pmuliw => "Pmuliw" | Pandiw => "Pandiw" | Pnandiw => "Pnandiw" @@ -1475,6 +1482,9 @@ Definition string_of_name_rri64 (n: arith_name_rri64): pstring := match n with Pcompil _ => "Pcompil" | Paddil => "Paddil" + | Psubil => "Psubil" + | Paddxil _ => "Paddxil" + | Psubxil _ => "Psubxil" | Pmulil => "Pmulil" | Pandil => "Pandil" | Pnandil => "Pnandil" @@ -1490,6 +1500,8 @@ Definition string_of_name_arrr (n: arith_name_arrr): pstring := match n with | Pmaddw => "Pmaddw" | Pmaddl => "Pmaddl" + | Pmsubw => "Pmsubw" + | Pmsubl => "Pmsubl" | Pcmove _ => "Pcmove" | Pcmoveu _ => "Pcmoveu" end. |