diff options
Diffstat (limited to 'cfrontend/SimplExpr.v')
| -rw-r--r-- | cfrontend/SimplExpr.v | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index 7cdff468..c7e57a54 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -268,8 +268,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 |