diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-20 15:07:15 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-20 15:07:15 +0200 |
| commit | f7a0149579078af35f90521acf7845adcfb22a02 (patch) | |
| tree | 5ea6052ead9ceb62690e5bd7a10627943a930e93 /powerpc/SelectOpproof.v | |
| parent | ed6043fe910f7a320f7af6d3f9d35f39f5cf7ee1 (diff) | |
| download | compcert-kvx-f7a0149579078af35f90521acf7845adcfb22a02.tar.gz compcert-kvx-f7a0149579078af35f90521acf7845adcfb22a02.zip | |
Added not merged destruction of Archi. Bug 17450
Diffstat (limited to 'powerpc/SelectOpproof.v')
| -rw-r--r-- | powerpc/SelectOpproof.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 757f1fd0..f93b93e5 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -838,6 +838,8 @@ Proof. intros. destruct x; simpl in H0; try discriminate. destruct (Float.to_intu f) as [n|] eqn:?; simpl in H0; inv H0. exists (Vint n); split; auto. unfold intuoffloat. + destruct Archi.ppc64. + econstructor. constructor; eauto. constructor. simpl; rewrite Heqo; auto. set (im := Int.repr Int.half_modulus). set (fm := Float.of_intu im). assert (eval_expr ge sp e m (Vfloat fm :: Vfloat f :: le) (Eletvar (S O)) (Vfloat f)). |