From 070babeff47562a72d6a58dd70fc7ac1bcbf205c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 15 Jun 2020 19:20:15 +0200 Subject: SimplExpr: better translation of casts in a "for effects" context This is useful for statements such as `(void) expr;` where we would prefer not to explicitly compute intermediate values of type `void` and store them in Clight temporary variables. See issue #361 for a real-world occurrence of this phenomenon. --- cfrontend/SimplExpr.v | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) (limited to 'cfrontend/SimplExpr.v') diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index 7cdff468..1398317d 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -226,6 +226,8 @@ Definition sd_seqbool_val (tmp: ident) (ty: type) := SDbase type_bool ty tmp. Definition sd_seqbool_set (ty: type) (sd: set_destination) := let tmp := sd_temp sd in SDcons type_bool ty tmp sd. +Definition sd_cast_set (ty: type) (sd: set_destination) := + let tmp := sd_temp sd in SDcons ty ty tmp sd. Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement * expr) := match a with @@ -268,8 +270,13 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement do (sl2, a2) <- transl_expr For_val r2; ret (finish dst (sl1 ++ sl2) (Ebinop op a1 a2 ty)) | Csyntax.Ecast r1 ty => - do (sl1, a1) <- transl_expr For_val r1; - ret (finish dst sl1 (Ecast a1 ty)) + match dst with + | For_val | For_set _ => + do (sl1, a1) <- transl_expr For_val r1; + ret (finish dst sl1 (Ecast a1 ty)) + | For_effects => + transl_expr For_effects r1 + end | Csyntax.Eseqand r1 r2 ty => do (sl1, a1) <- transl_expr For_val r1; match dst with -- cgit