diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-04 12:34:11 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-04 12:34:11 +0200 |
| commit | b7ded97f34c5f0c670f43f2b15e77eb8874a764e (patch) | |
| tree | df8cda7c77a4ee98ba9178be184a9e82ca5bbe84 /mppa_k1c/Op.v | |
| parent | 3b70f4b0eb0d8efde0946ed883072e0f94d5766d (diff) | |
| download | compcert-kvx-b7ded97f34c5f0c670f43f2b15e77eb8874a764e.tar.gz compcert-kvx-b7ded97f34c5f0c670f43f2b15e77eb8874a764e.zip | |
progressing on select
Diffstat (limited to 'mppa_k1c/Op.v')
| -rw-r--r-- | mppa_k1c/Op.v | 26 |
1 files changed, 10 insertions, 16 deletions
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 96df5e1f..c3ea4baf 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -1471,22 +1471,16 @@ Proof. - unfold eval_select. inv H4; trivial. inv H2; trivial. - inv H3; trivial. - + destruct (eval_condition0 cond _ m1) eqn:Hcond; trivial. - assert (Hcond' : ((eval_condition0 cond (Vint i1) m2) = Some b)). - * eapply eval_condition0_inj. - constructor. - assumption. - * rewrite Hcond'. constructor. - + destruct (eval_condition0 cond _ m1) eqn:Hcond; trivial. - assert (Hcond' : ((eval_condition0 cond (Vlong i1) m2) = Some b)). - - trivial. - exploit eval_condition0_inj; eauto. - exploit eval_condition0_inj; eauto. - destruct v; trivial. - destruct v0; trivial. - destruct v'; trivial. + inv H3; trivial; + try (destruct cond; simpl; trivial; fail). + destruct (eval_condition0 cond (Vptr _ _) m1) eqn:Hcond; trivial. + eassert (Hcond' : ((eval_condition0 cond (Vptr b2 (Ptrofs.add ofs1 (Ptrofs.repr delta)))) m2) = Some b). + * eapply eval_condition0_inj. + eapply Val.inject_ptr. + eassumption. + reflexivity. + assumption. + * rewrite Hcond'. constructor. (* selectl *) - inv H3; simpl; try constructor. inv H4; simpl; try constructor. |