diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-02-14 17:49:40 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-02-14 17:49:40 +0100 |
| commit | ed6e20995761614ee7ea6235b978a463f071c123 (patch) | |
| tree | c708063a2a911ae3d9b9caf1563151497b7670a5 /kvx/ValueAOp.v | |
| parent | fc384f172b72f90c8de52ec846344b7ffda76070 (diff) | |
| download | compcert-kvx-ed6e20995761614ee7ea6235b978a463f071c123.tar.gz compcert-kvx-ed6e20995761614ee7ea6235b978a463f071c123.zip | |
abs builtins
Diffstat (limited to 'kvx/ValueAOp.v')
| -rw-r--r-- | kvx/ValueAOp.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kvx/ValueAOp.v b/kvx/ValueAOp.v index f0fed567..ddfe94f3 100644 --- a/kvx/ValueAOp.v +++ b/kvx/ValueAOp.v @@ -157,10 +157,10 @@ Definition eval_static_insfl stop start prev fld := else Vtop. Definition absdiff := binop_int - (fun i1 i2 => Int.repr (ExtValues.int_abs_diff (Int.signed i1) (Int.signed i2))). + (fun i1 i2 => ExtValues.int_absdiff i1 i2). Definition absdiffl := binop_long - (fun i1 i2 => Int64.repr (ExtValues.int_abs_diff (Int64.signed i1) (Int64.signed i2))). + (fun i1 i2 => ExtValues.long_absdiff i1 i2). Definition eval_static_operation (op: operation) (vl: list aval): aval := match op, vl with |