diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-11 15:20:02 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-11 15:20:02 +0200 |
| commit | 2c428ad4e0177756db2f6dfe56831b5a44f6de5c (patch) | |
| tree | 1e209b6c935e36005b31542345ac8bb593361452 /mppa_k1c/Asmvliw.v | |
| parent | 3ef3e6c78026cc1d5793ccb4e905a0232ec7bb4e (diff) | |
| download | compcert-kvx-2c428ad4e0177756db2f6dfe56831b5a44f6de5c.tar.gz compcert-kvx-2c428ad4e0177756db2f6dfe56831b5a44f6de5c.zip | |
add with shift, beginning
Diffstat (limited to 'mppa_k1c/Asmvliw.v')
| -rw-r--r-- | mppa_k1c/Asmvliw.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index c1f21f8d..e1a7f916 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -1068,7 +1068,7 @@ Definition arith_eval_rrr n v1 v2 := | Pfmuld => Val.mulf v1 v2 | Pfmulw => Val.mulfs v1 v2 - | Paddxw shift => Val.add v2 (Val.shl v1 (Vint (int_of_shift1_4 shift))) + | Paddxw shift => ExtValues.addx (int_of_shift1_4 shift) v1 v2 | Paddxl shift => Val.addl v1 (Val.shll v1 (Vint (int_of_shift1_4 shift))) | Prevsubxw shift => Val.sub v2 (Val.shl v1 (Vint (int_of_shift1_4 shift))) @@ -1099,7 +1099,7 @@ Definition arith_eval_rri32 n v i := | Psrxil => ExtValues.val_shrxl v (Vint i) | Psrlil => Val.shrlu v (Vint i) | Psrail => Val.shrl v (Vint i) - | Paddxiw shift => Val.add (Vint i) (Val.shl v (Vint (int_of_shift1_4 shift))) + | Paddxiw shift => ExtValues.addx (int_of_shift1_4 shift) v (Vint i) | Prevsubxiw shift => Val.sub (Vint i) (Val.shl v (Vint (int_of_shift1_4 shift))) end. |