diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-30 12:00:33 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-30 12:00:33 +0200 |
| commit | c455f69d66b186414c8bb1c5cd28ce8f29e965aa (patch) | |
| tree | 569ef74216e5bce1e2a1d1457b0c8b930b14ef7e /aarch64/ValueAOp.v | |
| parent | 827bdabf1242720979848cf473263a54fcf212f5 (diff) | |
| download | compcert-kvx-c455f69d66b186414c8bb1c5cd28ce8f29e965aa.tar.gz compcert-kvx-c455f69d66b186414c8bb1c5cd28ce8f29e965aa.zip | |
AArch64 division no longer "traps"
Diffstat (limited to 'aarch64/ValueAOp.v')
| -rw-r--r-- | aarch64/ValueAOp.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/aarch64/ValueAOp.v b/aarch64/ValueAOp.v index e0d98c85..d379bbe8 100644 --- a/aarch64/ValueAOp.v +++ b/aarch64/ValueAOp.v @@ -96,8 +96,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Omul, v1::v2::nil => mul v1 v2 | Omuladd, v1::v2::v3::nil => add v1 (mul v2 v3) | Omulsub, v1::v2::v3::nil => sub v1 (mul v2 v3) - | Odiv, v1::v2::nil => divs v1 v2 - | Odivu, v1::v2::nil => divu v1 v2 + | Odiv, v1::v2::nil => divs_total v1 v2 + | Odivu, v1::v2::nil => divu_total v1 v2 | Oand, v1::v2::nil => and v1 v2 | Oandshift s a, v1::v2::nil => and v1 (eval_static_shift s v2 a) | Oandimm n, v1::nil => and v1 (I n) @@ -145,8 +145,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Omullsub, v1::v2::v3::nil => subl v1 (mull v2 v3) | Omullhs, v1::v2::nil => mullhs v1 v2 | Omullhu, v1::v2::nil => mullhu v1 v2 - | Odivl, v1::v2::nil => divls v1 v2 - | Odivlu, v1::v2::nil => divlu v1 v2 + | Odivl, v1::v2::nil => divls_total v1 v2 + | Odivlu, v1::v2::nil => divlu_total v1 v2 | Oandl, v1::v2::nil => andl v1 v2 | Oandlshift s a, v1::v2::nil => andl v1 (eval_static_shiftl s v2 a) | Oandlimm n, v1::nil => andl v1 (L n) |