aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/Asmblockdeps.v
diff options
context:
space:
mode:
Diffstat (limited to 'aarch64/Asmblockdeps.v')
-rw-r--r--aarch64/Asmblockdeps.v12
1 files changed, 6 insertions, 6 deletions
diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v
index 670a7d06..e1d591df 100644
--- a/aarch64/Asmblockdeps.v
+++ b/aarch64/Asmblockdeps.v
@@ -211,14 +211,14 @@ Coercion Control: control_op >-> op_wrap.
Definition v_compare_int (v1 v2: val) : CRflags :=
{| _CN := (Val.negative (Val.sub v1 v2));
- _CZ := (Val_cmpu Ceq v1 v2);
- _CC := (Val_cmpu Cge v1 v2);
+ _CZ := (Val.mxcmpu Ceq v1 v2);
+ _CC := (Val.mxcmpu Cge v1 v2);
_CV := (Val.sub_overflow v1 v2) |}.
Definition v_compare_long (v1 v2: val) : CRflags :=
{| _CN := (Val.negativel (Val.subl v1 v2));
- _CZ := (Val_cmplu Ceq v1 v2);
- _CC := (Val_cmplu Cge v1 v2);
+ _CZ := (Val.mxcmplu Ceq v1 v2);
+ _CC := (Val.mxcmplu Cge v1 v2);
_CV := (Val.subl_overflow v1 v2) |}.
Definition v_compare_float (v1 v2: val) : CRflags :=
@@ -1842,8 +1842,8 @@ Proof.
destruct (PregEq.eq r PC);
[ rewrite e; destruct sz0; simpl; Simpl sr |
destruct sz0; simpl; replace_pc; rewrite Pregmap.gso; auto; repeat Simpl_rep sr; try rewrite H0;
- try (destruct (Val_cmpu_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b);
- try (destruct (Val_cmplu_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b);
+ try (destruct (Val.mxcmpu_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b);
+ try (destruct (Val.mxcmplu_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b);
try (destruct (Val.cmp_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b);
try (destruct (Val.cmpl_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b);
try (simpl; rewrite sr_update_overwrite; replace_pc; Simpl sr);