From a75a8f1270766351815aa73fbe114c9f100162ce Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Tue, 27 Mar 2012 14:35:15 +0000
Subject: [PATCH] Printing the loop invariant
---
src/main/scala/leon/purescala/PrettyPrinter.scala | 13 ++++++++++++-
1 file changed, 12 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index dc287b62d..ec7236d50 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -110,7 +110,18 @@ object PrettyPrinter {
sb
}
case Assignment(lhs, rhs) => ppBinary(sb, lhs.toVariable, rhs, " = ", lvl)
- case While(cond, body) => {
+ case wh@While(cond, body) => {
+ wh.invariant match {
+ case Some(inv) => {
+ sb.append("\n")
+ ind(sb, lvl)
+ sb.append("@invariant: ")
+ pp(inv, sb, lvl)
+ sb.append("\n")
+ ind(sb, lvl)
+ }
+ case None =>
+ }
sb.append("while(")
pp(cond, sb, lvl)
sb.append(")\n")
--
GitLab