From 7ea8a55692e2a2d32efa0c84e19c37a3b56a0fd1 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 19 Aug 2011 09:13:09 +0000 Subject: Cleaned up old commented-out parts git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1719 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Csem.v | 34 ---------------------------------- 1 file changed, 34 deletions(-) (limited to 'cfrontend/Csem.v') diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 90bb2e31..426a7536 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -61,40 +61,6 @@ Definition cast_float_float (sz: floatsize) (f: float) : float := | F64 => f end. -(* -Definition neutral_for_cast (t: type) : bool := - match t with - | Tint I32 sg => true - | Tpointer ty => true - | Tarray ty sz => true - | Tfunction targs tres => true - | _ => false - end. - -Function sem_cast (v: val) (t1 t2: type) : option val := - match v, t1, t2 with - | Vint i, Tint sz1 si1, Tint sz2 si2 => (**r int to int *) - Some (Vint (cast_int_int sz2 si2 i)) - | Vfloat f, Tfloat sz1, Tint sz2 si2 => (**r float to int *) - match cast_float_int si2 f with - | Some i => Some (Vint (cast_int_int sz2 si2 i)) - | None => None - end - | Vint i, Tint sz1 si1, Tfloat sz2 => (**r int to float *) - Some (Vfloat (cast_float_float sz2 (cast_int_float si1 i))) - | Vfloat f, Tfloat sz1, Tfloat sz2 => (**r float to float *) - Some (Vfloat (cast_float_float sz2 f)) - | Vptr b ofs, _, _ => (**r int32|pointer to int32|pointer *) - if neutral_for_cast t1 && neutral_for_cast t2 - then Some(Vptr b ofs) else None - | Vint n, _, _ => (**r int32|pointer to int32|pointer *) - if neutral_for_cast t1 && neutral_for_cast t2 - then Some(Vint n) else None - | _, _, _ => - None - end. -*) - Function sem_cast (v: val) (t1 t2: type) : option val := match classify_cast t1 t2 with | cast_case_neutral => -- cgit