From bd5ec2055fce4bd8adadbf4dcd6e891c0fc66c92 Mon Sep 17 00:00:00 2001
From: Marco Antognini <antognini.marco@gmail.com>
Date: Tue, 1 Dec 2015 21:13:01 +0100
Subject: [PATCH] Remove code duplication in translated while statement
---
src/main/scala/leon/genc/CConverter.scala | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/genc/CConverter.scala b/src/main/scala/leon/genc/CConverter.scala
index 05a7f2c38..a29943083 100644
--- a/src/main/scala/leon/genc/CConverter.scala
+++ b/src/main/scala/leon/genc/CConverter.scala
@@ -413,8 +413,8 @@ class CConverter(val ctx: LeonContext, val prog: Program) {
// Transform while (cond) { body } into
// while (true) { if (cond) { body } else { break } }
val condF = flatten(cond)
- val ifelse = condF.body ~~ buildIfElse(condF.value, body, CAST.Break)
- CAST.While(CAST.True, ifelse)
+ val ifelse = condF.body ~~ buildIfElse(condF.value, CAST.NoStmt, CAST.Break)
+ CAST.While(CAST.True, ifelse ~ body)
}
case FunctionInvocation(tfd @ TypedFunDef(fd, _), stdArgs) =>
--
GitLab