diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-02 09:32:49 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-02 09:32:49 +0200 |
| commit | 9f256a4ad30c93749e6c1192a84f996feac3b023 (patch) | |
| tree | 81b381e5651e34474a133f012927442f64d51c56 /mppa_k1c/SelectOpproof.v | |
| parent | 053cfa54205575ceb984f5922f51f4fce5980604 (diff) | |
| download | compcert-kvx-9f256a4ad30c93749e6c1192a84f996feac3b023.tar.gz compcert-kvx-9f256a4ad30c93749e6c1192a84f996feac3b023.zip | |
command line options (still incomplete)
Diffstat (limited to 'mppa_k1c/SelectOpproof.v')
| -rw-r--r-- | mppa_k1c/SelectOpproof.v | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index a92ed572..9e2eec8b 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -1256,7 +1256,7 @@ Theorem eval_addressing: Proof. intros until v. unfold addressing; case (addressing_match a); intros; InvEval. - exists (@nil val); split. eauto with evalexpr. simpl. auto. - - destruct (Archi.pic_code tt). + - destruct (orb _ _). + exists (Vptr b ofs0 :: nil); split. constructor. EvalOp. simpl. congruence. constructor. simpl. rewrite Ptrofs.add_zero. congruence. + exists (@nil val); split. constructor. simpl; auto. @@ -1265,11 +1265,18 @@ Proof. - exists (v1 :: nil); split. eauto with evalexpr. simpl. destruct v1; simpl in H; try discriminate. destruct Archi.ptr64 eqn:SF; inv H. simpl. auto. - - destruct (Z.eq_dec _ _). - + exists (v1 :: v2 :: nil); split. repeat (constructor; auto). simpl. rewrite Int.repr_unsigned. destruct v2; simpl in *; congruence. - + exists (v1 :: v0 :: nil); split. repeat (constructor; auto). econstructor. - repeat (constructor; auto). eassumption. simpl. congruence. - simpl. congruence. + - destruct (Compopts.optim_fxsaddr tt). + + destruct (Z.eq_dec _ _). + * exists (v1 :: v2 :: nil); split. + repeat (constructor; auto). simpl. rewrite Int.repr_unsigned. destruct v2; simpl in *; congruence. + * exists (v1 :: v0 :: nil); split. + repeat (constructor; auto). econstructor. + repeat (constructor; auto). eassumption. simpl. congruence. + simpl. congruence. + + exists (v1 :: v0 :: nil); split. + repeat (constructor; auto). econstructor. + repeat (constructor; auto). eassumption. simpl. congruence. + simpl. congruence. - exists (v1 :: v0 :: nil); split. repeat (constructor; auto). simpl. congruence. - exists (v :: nil); split. eauto with evalexpr. subst. simpl. rewrite Ptrofs.add_zero; auto. Qed. |