From 728888d8a3f70afd526f6c4454327f52ea4c4746 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 7 Jan 2021 17:47:55 +0100 Subject: Val_cmp* -> Val.mxcmp* --- aarch64/Asmblockdeps.v | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'aarch64/Asmblockdeps.v') 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); -- cgit