diff options
| author |  stefanheule <unknown> | 2012-03-13 04:45:51 -0700 |
|---|---|---|
| committer | stefanheule <unknown> | 2012-03-13 04:45:51 -0700 |
| commit | e7534575867b8439af0ce747ea14e32f222cec92 (patch) | |
| tree | a545eff7656bfff73cf0c62d12158c355ef07656 | |
| parent | 1d0b23b71e9bd9838042098bac1ba731f373c680 (diff) | |
Chalice: Do not print empty conditionals.
| -rw-r--r-- | Chalice/src/main/scala/Boogie.scala | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/Chalice/src/main/scala/Boogie.scala b/Chalice/src/main/scala/Boogie.scala index acc061ad..900ad6d1 100644 --- a/Chalice/src/main/scala/Boogie.scala +++ b/Chalice/src/main/scala/Boogie.scala @@ -222,13 +222,17 @@ object Boogie { indent + "assert " + "{:msg \"" + pos + assert.message + "\"}" + (assert.subsumption match {case Some(n) => "{:subsumption " + n + "}"; case None => ""}) + " " + PrintExpr(e) + ";" + nl
case Assume(e) => indent + "assume " + PrintExpr(e) + ";" + nl
case If(guard, thn, els) =>
+ if (thn == Nil && els == Nil) "" else
indent + "if (" +
(if (guard == null) "*" else PrintExpr(guard)) +
") {" + nl +
IndentMore { Print(thn, "", PrintStmt) } +
- indent + "} else {" + nl +
- IndentMore { Print(els, "", PrintStmt) } +
- indent + "}" + nl
+ indent + "}" +
+ (if (els == Nil) nl else
+ " else {" + nl +
+ IndentMore { Print(els, "", PrintStmt) } +
+ indent + "}" + nl
+ )
case Assign(lhs, rhs) =>
indent + PrintExpr(lhs) + " := " + PrintExpr(rhs) + ";" + nl
case AssignMap(lhs, index, rhs) =>
|