From 6ce07727bcf4e330f897d9461a924334a0f0980e Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Tue, 21 Mar 2017 15:22:46 +0100 Subject: attempt to optimize empty if/then/else statements --- cfrontend/SimplExpr.v | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'cfrontend/SimplExpr.v') diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index 8725edd1..a5306b4b 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -436,7 +436,10 @@ Fixpoint transl_stmt (s: Csyntax.statement) : mon statement := do ts1 <- transl_stmt s1; do ts2 <- transl_stmt s2; do (s', a) <- transl_expression e; - ret (Ssequence s' (Sifthenelse a ts1 ts2)) + if is_Sskip s1 && is_Sskip s2 then + ret (Ssequence s' Sskip) + else + ret (Ssequence s' (Sifthenelse a ts1 ts2)) | Csyntax.Swhile e s1 => do s' <- transl_if e Sskip Sbreak; do ts1 <- transl_stmt s1; -- cgit