diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-07-04 17:49:11 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-07-17 09:17:28 +0200 |
| commit | 633e60ed36c07c4b6cb4b1dc93b9eea312882ceb (patch) | |
| tree | 22feeaf195a61a3ffecf280717ddbde60987a5c7 /cfrontend/Cop.v | |
| parent | 10aa130361a5a673a14a7b38ed9c077103f9155f (diff) | |
| download | compcert-kvx-633e60ed36c07c4b6cb4b1dc93b9eea312882ceb.tar.gz compcert-kvx-633e60ed36c07c4b6cb4b1dc93b9eea312882ceb.zip | |
Make __builtin_sel available from C source code
It is type-checked like a conditional expression then translated to
a call to the known builtin function.
Diffstat (limited to 'cfrontend/Cop.v')
| -rw-r--r-- | cfrontend/Cop.v | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v index c395a2cb..782fb32a 100644 --- a/cfrontend/Cop.v +++ b/cfrontend/Cop.v @@ -1580,6 +1580,27 @@ Proof. intros. apply cast_val_casted. eapply cast_val_is_casted; eauto. Qed. +(** Moreover, casted values belong to the machine type corresponding to the + C type. *) + +Lemma val_casted_has_type: + forall v ty, val_casted v ty -> ty <> Tvoid -> Val.has_type v (typ_of_type ty). +Proof. + intros. inv H; simpl typ_of_type. +- exact I. +- exact I. +- exact I. +- exact I. +- apply Val.Vptr_has_type. +- red; unfold Tptr; rewrite H1; auto. +- red; unfold Tptr; rewrite H1; auto. +- red; unfold Tptr; rewrite H1; auto. +- red; unfold Tptr; rewrite H1; auto. +- apply Val.Vptr_has_type. +- apply Val.Vptr_has_type. +- congruence. +Qed. + (** Relation with the arithmetic conversions of ISO C99, section 6.3.1 *) Module ArithConv. |