diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-01-07 17:47:55 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-01-07 17:47:55 +0100 |
| commit | 728888d8a3f70afd526f6c4454327f52ea4c4746 (patch) | |
| tree | c0e57b9ec1de6c5580bdf296d85a3024af738537 /aarch64/Asmblockdeps.v | |
| parent | ac8b7ae094cf7741fec63effd8fcfd1467fb2edf (diff) | |
| download | compcert-kvx-728888d8a3f70afd526f6c4454327f52ea4c4746.tar.gz compcert-kvx-728888d8a3f70afd526f6c4454327f52ea4c4746.zip | |
Val_cmp* -> Val.mxcmp*
Diffstat (limited to 'aarch64/Asmblockdeps.v')
| -rw-r--r-- | aarch64/Asmblockdeps.v | 12 |
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); |