diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-04-09 11:02:52 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-04-09 11:02:52 +0200 |
| commit | b7720bc5973e9890e7c320bb34b784e2e2b2da69 (patch) | |
| tree | 7c4dca4a00586bb9c6f2aaeec24e64a6dc77077f /riscV/Asmgenproof1.v | |
| parent | 2f2e7b1da225aa3bf066c2fc689a08fab9851a53 (diff) | |
| download | compcert-kvx-b7720bc5973e9890e7c320bb34b784e2e2b2da69.tar.gz compcert-kvx-b7720bc5973e9890e7c320bb34b784e2e2b2da69.zip | |
Removing addptrofs draft, next will be merging
Diffstat (limited to 'riscV/Asmgenproof1.v')
| -rw-r--r-- | riscV/Asmgenproof1.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index cbe68577..2293e001 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -1274,7 +1274,7 @@ Opaque Int.eq. { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). exists rs'; split. eexact A. eauto with asmgen. } (* Expanded instructions from RTL *) - 8,9,17,18: + 9,10,19,20: econstructor; split; try apply exec_straight_one; simpl; eauto; split; intros; Simpl; try destruct (rs x0); try rewrite Int64.add_commut; @@ -1283,9 +1283,8 @@ Opaque Int.eq. try rewrite Int.and_commut; auto; try rewrite Int64.or_commut; try rewrite Int.or_commut; auto. - 1-14: + 1-16: destruct optR as [[]|]; try discriminate; - try (ArgsInv; simpl in EV; SimplEval EV; try TranslOpSimpl); unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; try inv EQ3; try inv EQ2; try destruct (Int.eq _ _) eqn:A; try inv H0; try destruct (Int64.eq _ _) eqn:A; try inv H1; |