diff options
| author | Michael Schmidt <github@mschmidt.me> | 2017-03-21 15:22:46 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-04-06 15:16:11 +0200 |
| commit | 6ce07727bcf4e330f897d9461a924334a0f0980e (patch) | |
| tree | 96550377c581d69a61f89069175497dbe7cf725d /cfrontend/SimplExpr.v | |
| parent | 8d4562d4d3bebb9c62374beaf39d8327acdc647d (diff) | |
| download | compcert-kvx-6ce07727bcf4e330f897d9461a924334a0f0980e.tar.gz compcert-kvx-6ce07727bcf4e330f897d9461a924334a0f0980e.zip | |
attempt to optimize empty if/then/else statements
Diffstat (limited to 'cfrontend/SimplExpr.v')
| -rw-r--r-- | cfrontend/SimplExpr.v | 5 |
1 files changed, 4 insertions, 1 deletions
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; |