diff options
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 |