From a3c1aed82d88df7592e63531dc8ce24482da1c28 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 17 Nov 2016 13:39:06 +0100 Subject: Initializers: introduce 'constval_cast' to cast constant value to desired type This comes handy in the next commit where constval_cast is used from C2C. --- cfrontend/Initializers.v | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'cfrontend/Initializers.v') diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index 19518aea..388b6544 100644 --- a/cfrontend/Initializers.v +++ b/cfrontend/Initializers.v @@ -133,6 +133,11 @@ Fixpoint constval (ce: composite_env) (a: expr) : res val := Error(msg "not a compile-time constant") end. +(** [constval_cast ce a ty] evaluates [a] then converts its value to type [ty]. *) + +Definition constval_cast (ce: composite_env) (a: expr) (ty: type): res val := + do v <- constval ce a; do_cast v (typeof a) ty. + (** * Translation of initializers *) Inductive initializer := @@ -148,9 +153,8 @@ with initializer_list := of type [ty]. Return the corresponding initialization datum. *) Definition transl_init_single (ce: composite_env) (ty: type) (a: expr) : res init_data := - do v1 <- constval ce a; - do v2 <- do_cast v1 (typeof a) ty; - match v2, ty with + do v <- constval_cast ce a ty; + match v, ty with | Vint n, Tint (I8|IBool) sg _ => OK(Init_int8 n) | Vint n, Tint I16 sg _ => OK(Init_int16 n) | Vint n, Tint I32 sg _ => OK(Init_int32 n) -- cgit