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/Cshmgen.v | 29 ++++++++++++++++++++++++++++- 1 file changed, 28 insertions(+), 1 deletion(-) (limited to 'cfrontend/Cshmgen.v') diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index e32001b9..9856b9ef 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -214,7 +214,7 @@ Definition make_cmp (c: comparison) (e1: expr) (ty1: type) (e2: expr) (ty2: type - [make_cast1] converts from integers to floats or from floats to integers; - [make_cast2] converts to a "small" int or float type if necessary. *) - +(* Definition make_cast1 (from to: type) (e: expr) := match from, to with | Tint _ uns, Tfloat _ => make_floatofint e uns @@ -234,6 +234,33 @@ Definition make_cast2 (from to: type) (e: expr) := Definition make_cast (from to: type) (e: expr) := make_cast2 from to (make_cast1 from to e). +*) + +Definition make_cast_int (e: expr) (sz: intsize) (si: signedness) := + match sz, si with + | I8, Signed => Eunop Ocast8signed e + | I8, Unsigned => Eunop Ocast8unsigned e + | I16, Signed => Eunop Ocast16signed e + | I16, Unsigned => Eunop Ocast16unsigned e + | I32, _ => e + end. + +Definition make_cast_float (e: expr) (sz: floatsize) := + match sz with + | F32 => Eunop Osingleoffloat e + | F64 => e + end. + +Definition make_cast (from to: type) (e: expr) := + match classify_cast from to with + | cast_case_neutral => e + | cast_case_i2i sz2 si2 => make_cast_int e sz2 si2 + | cast_case_f2f sz2 => make_cast_float e sz2 + | cast_case_i2f si1 sz2 => make_cast_float (make_floatofint e si1) sz2 + | cast_case_f2i sz2 si2 => make_cast_int (make_intoffloat e si2) sz2 si2 + | cast_case_void => e + | cast_case_default => e + end. (** [make_load addr ty_res] loads a value of type [ty_res] from the memory location denoted by the Csharpminor expression [addr]. -- cgit