diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-05-22 10:12:19 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-05-22 10:12:19 +0200 |
| commit | 5dd1544021c608060d8ee5ba052cc82132fff741 (patch) | |
| tree | 29ca8d8e653b0b1d10e02a16368437458f87e672 /cfrontend/Ctyping.v | |
| parent | b686f8df572ea77c8832637bed4e4cd81f0931e2 (diff) | |
| download | compcert-kvx-5dd1544021c608060d8ee5ba052cc82132fff741.tar.gz compcert-kvx-5dd1544021c608060d8ee5ba052cc82132fff741.zip | |
Missing case in type_conditional (long long vs. int or float).
Diffstat (limited to 'cfrontend/Ctyping.v')
| -rw-r--r-- | cfrontend/Ctyping.v | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index 834895bc..d726a525 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -243,7 +243,8 @@ Definition is_void (ty: type) : bool := Definition type_conditional (ty1 ty2: type) : res type := match typeconv ty1, typeconv ty2 with - | (Tint _ _ _ | Tfloat _ _), (Tint _ _ _ | Tfloat _ _) => + | (Tint _ _ _ | Tlong _ _ | Tfloat _ _), + (Tint _ _ _ | Tlong _ _ | Tfloat _ _) => binarith_type ty1 ty2 "conditional expression" | Tpointer t1 a1, Tpointer t2 a2 => let t := @@ -1011,13 +1012,9 @@ Proof. apply A. apply A. } clear A. unfold type_conditional in H. destruct (typeconv t1) eqn:T1; try discriminate; - destruct (typeconv t2) eqn:T2; inv H; auto using D. -- eapply binarith_type_cast; eauto. -- eapply binarith_type_cast; eauto. + destruct (typeconv t2) eqn:T2; inv H; eauto using D, binarith_type_cast. - split; apply typeconv_cast; unfold wt_cast. rewrite T1; simpl; congruence. rewrite T2; simpl; congruence. -- eapply binarith_type_cast; eauto. -- eapply binarith_type_cast; eauto. - split; apply typeconv_cast; unfold wt_cast. rewrite T1; simpl; congruence. rewrite T2; simpl; congruence. - split; apply typeconv_cast; unfold wt_cast. |