diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-01-07 18:21:55 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-01-07 18:21:55 +0100 |
| commit | 10da6dfa77f155d9d1e36e28c8bb8552601355f9 (patch) | |
| tree | c04e52f494b1d41c5616d55d6e95e805cce69a60 /kvx/Asmblockdeps.v | |
| parent | 728888d8a3f70afd526f6c4454327f52ea4c4746 (diff) | |
| download | compcert-kvx-10da6dfa77f155d9d1e36e28c8bb8552601355f9.tar.gz compcert-kvx-10da6dfa77f155d9d1e36e28c8bb8552601355f9.zip | |
update kvx
Diffstat (limited to 'kvx/Asmblockdeps.v')
| -rw-r--r-- | kvx/Asmblockdeps.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kvx/Asmblockdeps.v b/kvx/Asmblockdeps.v index 67430b54..b6d18c3e 100644 --- a/kvx/Asmblockdeps.v +++ b/kvx/Asmblockdeps.v @@ -398,8 +398,8 @@ Definition control_eval (o: control_op) (l: list value) := end | Ocbu bt l, [Val v; Val vpc] => match cmpu_for_btest bt with - | (Some c, Int) => eval_branch_deps fn l vpc (Val_cmpu_bool c v (Vint (Int.repr 0))) - | (Some c, Long) => eval_branch_deps fn l vpc (Val_cmplu_bool c v (Vlong (Int64.repr 0))) + | (Some c, Int) => eval_branch_deps fn l vpc (Val.mxcmpu_bool c v (Vint (Int.repr 0))) + | (Some c, Long) => eval_branch_deps fn l vpc (Val.mxcmplu_bool c v (Vlong (Int64.repr 0))) | (None, _) => None end | Odiv, [Val v1; Val v2] => @@ -1232,12 +1232,12 @@ Proof. (* Pcbu *) + rewrite (H0 PC). Simpl. rewrite (H0 r). destruct (cmpu_for_btest _); simpl; auto. destruct o; simpl; auto. unfold par_eval_branch. unfold eval_branch_deps. unfold incrPC. Simpl. destruct i. - ++ destruct (Val_cmpu_bool _ _ _); simpl; auto. destruct b. + ++ destruct (Val.mxcmpu_bool _ _ _); simpl; auto. destruct b. +++ unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl. destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. +++ repeat (econstructor; eauto). intros rr; destruct rr; Simpl. - ++ destruct (Val_cmplu_bool _ _ _); simpl; auto. destruct b. + ++ destruct (Val.mxcmplu_bool _ _ _); simpl; auto. destruct b. +++ unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl. destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. |