From 335c01eba7bfca53e9f44bbe74e9321475c4d012 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 17 Jul 2011 17:11:44 +0000 Subject: Improved semantics of casts git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1685 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Csyntax.v | 23 ++++++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-) (limited to 'cfrontend/Csyntax.v') diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index a199f33..c76d9b9 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -662,7 +662,7 @@ Definition access_mode (ty: type) : mode := | Tfunction _ _ => By_reference | Tstruct _ fList => By_nothing | Tunion _ fList => By_nothing - | Tcomp_ptr _ => By_value Mint32 + | Tcomp_ptr _ => By_nothing end. (** Unroll the type of a structure or union field, substituting @@ -925,6 +925,27 @@ Definition classify_fun (ty: type) := | _ => fun_default end. +Inductive classify_cast_cases : Type := + | cast_case_neutral (**r int|pointer -> int32|pointer *) + | cast_case_i2i (sz2:intsize) (si2:signedness) (**r int -> int *) + | cast_case_f2f (sz2:floatsize) (**r float -> float *) + | cast_case_i2f (si1:signedness) (sz2:floatsize) (**r int -> float *) + | cast_case_f2i (sz2:intsize) (si2:signedness) (**r float -> int *) + | cast_case_void (**r any -> void *) + | cast_case_default. + +Function classify_cast (tfrom tto: type) : classify_cast_cases := + match tto, tfrom with + | Tint I32 si2, (Tint _ _ | Tpointer _ | Tarray _ _ | Tfunction _ _) => cast_case_neutral + | Tint sz2 si2, Tint sz1 si1 => cast_case_i2i sz2 si2 + | Tint sz2 si2, Tfloat sz1 => cast_case_f2i sz2 si2 + | Tfloat sz2, Tfloat sz1 => cast_case_f2f sz2 + | Tfloat sz2, Tint sz1 si1 => cast_case_i2f si1 sz2 + | Tpointer _, (Tint _ _ | Tpointer _ | Tarray _ _ | Tfunction _ _) => cast_case_neutral + | Tvoid, _ => cast_case_void + | _, _ => cast_case_default + end. + (** Translating C types to Cminor types, function signatures, and external functions. *) -- cgit v1.2.3