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.

1 files changed, 9 insertions, 2 deletions

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