diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-05-06 15:25:26 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-05-06 15:25:26 +0000 |
| commit | 884756b623fd6031a04102a545d92e4ec905f1cc (patch) | |
| tree | 9e2804da54087bbcb44df675432dcb133294b8b6 /cfrontend/Cshmgenproof.v | |
| parent | 76555ffd2403b3ebf1ea353063c16763e6493722 (diff) | |
Revised semantics and compilation of 2-argument C operators to better match
"the usual binary conversions" and be more robust towards future extensions
e.g. with 32-bit float values.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2239 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/Cshmgenproof.v')
| -rw-r--r-- | cfrontend/Cshmgenproof.v | 36 |
1 files changed, 18 insertions, 18 deletions
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index de3b8df..953e690 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -377,21 +377,19 @@ Lemma make_binarith_correct: (sem_binarith sem_int sem_long sem_float). Proof. red; unfold make_binarith, sem_binarith; - intros until m; intros SEM MAKE EV1 EV2; - destruct (classify_binarith tya tyb); inv MAKE; - destruct va; try discriminate; destruct vb; try discriminate. + intros until m; intros SEM MAKE EV1 EV2. + set (cls := classify_binarith tya tyb) in *. + set (ty := binarith_type cls) in *. + monadInv MAKE. + destruct (sem_cast va tya ty) as [va'|] eqn:Ca; try discriminate. + destruct (sem_cast vb tyb ty) as [vb'|] eqn:Cb; try discriminate. + exploit make_cast_correct. eexact EQ. eauto. eauto. intros EV1'. + exploit make_cast_correct. eexact EQ1. eauto. eauto. intros EV2'. + destruct cls; inv EQ2; destruct va'; try discriminate; destruct vb'; try discriminate. - destruct s; inv H0; econstructor; eauto with cshm. rewrite iop_ok; auto. rewrite iopu_ok; auto. -- erewrite <- fop_ok in SEM; eauto with cshm. -- erewrite <- fop_ok in SEM; eauto with cshm. -- erewrite <- fop_ok in SEM; eauto with cshm. - destruct s; inv H0; econstructor; eauto with cshm. rewrite lop_ok; auto. rewrite lopu_ok; auto. -- destruct s2; inv H0; econstructor; eauto with cshm. - rewrite lop_ok; auto. rewrite lopu_ok; auto. -- destruct s1; inv H0; econstructor; eauto with cshm. - rewrite lop_ok; auto. rewrite lopu_ok; auto. -- erewrite <- fop_ok in SEM; eauto with cshm. - erewrite <- fop_ok in SEM; eauto with cshm. Qed. @@ -401,17 +399,19 @@ Lemma make_binarith_int_correct: (sem_binarith sem_int sem_long (fun x y => None)). Proof. red; unfold make_binarith_int, sem_binarith; - intros until m; intros SEM MAKE EV1 EV2; - destruct (classify_binarith tya tyb); inv MAKE; - destruct va; try discriminate; destruct vb; try discriminate. + intros until m; intros SEM MAKE EV1 EV2. + set (cls := classify_binarith tya tyb) in *. + set (ty := binarith_type cls) in *. + monadInv MAKE. + destruct (sem_cast va tya ty) as [va'|] eqn:Ca; try discriminate. + destruct (sem_cast vb tyb ty) as [vb'|] eqn:Cb; try discriminate. + exploit make_cast_correct. eexact EQ. eauto. eauto. intros EV1'. + exploit make_cast_correct. eexact EQ1. eauto. eauto. intros EV2'. + destruct cls; inv EQ2; destruct va'; try discriminate; destruct vb'; try discriminate. - destruct s; inv H0; econstructor; eauto with cshm. rewrite iop_ok; auto. rewrite iopu_ok; auto. - destruct s; inv H0; econstructor; eauto with cshm. rewrite lop_ok; auto. rewrite lopu_ok; auto. -- destruct s2; inv H0; econstructor; eauto with cshm. - rewrite lop_ok; auto. rewrite lopu_ok; auto. -- destruct s1; inv H0; econstructor; eauto with cshm. - rewrite lop_ok; auto. rewrite lopu_ok; auto. Qed. End MAKE_BIN. |