From 39bc6e4f98dabf672798893df990576542ac1675 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 29 Mar 2014 08:30:03 +0000 Subject: __builtin_absfloat can be applied to integers too. More precise classification of float results of arithmetic operations, in preparation for future work on the C/Clight static type system. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2441 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cshmgen.v | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) (limited to 'cfrontend/Cshmgen.v') diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 1380695..c97e881 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -164,11 +164,19 @@ Definition make_notbool (e: expr) (ty: type) := Definition make_neg (e: expr) (ty: type) := match classify_neg ty with | neg_case_i _ => OK (Eunop Onegint e) - | neg_case_f => OK (Eunop Onegf e) + | neg_case_f _ => OK (Eunop Onegf e) | neg_case_l _ => OK (Eunop Onegl e) | _ => Error (msg "Cshmgen.make_neg") end. +Definition make_absfloat (e: expr) (ty: type) := + match classify_neg ty with + | neg_case_i sg => OK (Eunop Oabsf (make_floatofint e sg F64)) + | neg_case_f _ => OK (Eunop Oabsf e) + | neg_case_l sg => OK (Eunop Oabsf (make_floatoflong e sg F64)) + | _ => Error (msg "Cshmgen.make_absfloat") + end. + Definition make_notint (e: expr) (ty: type) := match classify_notint ty with | notint_case_i _ => OK (Eunop Onotint e) @@ -187,7 +195,7 @@ Definition make_binarith (iop iopu fop lop lopu: binary_operation) match c with | bin_case_i Signed => OK (Ebinop iop e1' e2') | bin_case_i Unsigned => OK (Ebinop iopu e1' e2') - | bin_case_f => OK (Ebinop fop e1' e2') + | bin_case_f _ => OK (Ebinop fop e1' e2') | bin_case_l Signed => OK (Ebinop lop e1' e2') | bin_case_l Unsigned => OK (Ebinop lopu e1' e2') | bin_default => Error (msg "Cshmgen.make_binarith") @@ -243,7 +251,7 @@ Definition make_binarith_int (iop iopu lop lopu: binary_operation) | bin_case_i Unsigned => OK (Ebinop iopu e1' e2') | bin_case_l Signed => OK (Ebinop lop e1' e2') | bin_case_l Unsigned => OK (Ebinop lopu e1' e2') - | bin_case_f | bin_default => Error (msg "Cshmgen.make_binarith_int") + | bin_case_f _ | bin_default => Error (msg "Cshmgen.make_binarith_int") end. Definition make_mod (e1: expr) (ty1: type) (e2: expr) (ty2: type) := @@ -329,7 +337,7 @@ Definition transl_unop (op: Cop.unary_operation) (a: expr) (ta: type) : res expr | Cop.Onotbool => make_notbool a ta | Cop.Onotint => make_notint a ta | Cop.Oneg => make_neg a ta - | Cop.Oabsfloat => OK (Eunop Oabsf a) + | Cop.Oabsfloat => make_absfloat a ta end. Definition transl_binop (op: Cop.binary_operation) -- cgit v1.2.3