From 32bdcd0acf2a5772620579ea4b2cfa9d993e6959 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Tue, 26 May 2015 14:22:31 +0200
Subject: [PATCH] Print program after xlang transformation in debug
---
src/main/scala/leon/xlang/XLangAnalysisPhase.scala | 7 +++++++
1 file changed, 7 insertions(+)
diff --git a/src/main/scala/leon/xlang/XLangAnalysisPhase.scala b/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
index 94e94a858..f6d535767 100644
--- a/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
+++ b/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
@@ -6,6 +6,8 @@ package xlang
import leon.purescala.Definitions._
import leon.verification._
+import leon.utils._
+
object XLangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
val name = "xlang analysis"
@@ -23,6 +25,11 @@ object XLangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
val (pgm1, wasLoop) = ImperativeCodeElimination.run(ctx)(pgm)
val pgm2 = purescala.FunctionClosure.run(ctx)(pgm1)
+ if (ctx.reporter.isDebugEnabled(DebugSectionTrees)) {
+ PrintTreePhase("Program after xlang transformations").run(ctx)(pgm2)
+ }
+
+
def functionWasLoop(fd: FunDef): Boolean = fd.orig match {
case Some(nested) => // could have been a LetDef originally
wasLoop.contains(nested)
--
GitLab