From e7ffc49cbd823eac14c7130b7422d2e6c99b1667 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 9 Oct 2015 18:06:46 +0200
Subject: [PATCH] Display more information in case of a verification failure
---
.../leon/regression/verification/VerificationSuite.scala | 9 +++++++--
src/test/scala/leon/test/LeonRegressionSuite.scala | 2 +-
2 files changed, 8 insertions(+), 3 deletions(-)
diff --git a/src/test/scala/leon/regression/verification/VerificationSuite.scala b/src/test/scala/leon/regression/verification/VerificationSuite.scala
index 2460d7791..48fdd4169 100644
--- a/src/test/scala/leon/regression/verification/VerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/VerificationSuite.scala
@@ -61,8 +61,13 @@ trait VerificationSuite extends LeonRegressionSuite {
ts(f"$index%3d: $displayName ${options.mkString(" ")}", Seq()) {
val ctx = createLeonContext(options: _*)
- val (ctx2, report) = analysis.run(ctx, p)
- block(Output(report, ctx2.reporter))
+ try {
+ val (ctx2, report) = analysis.run(ctx, p)
+ block(Output(report, ctx2.reporter))
+ } catch {
+ case fe: LeonFatalError =>
+ fail(ctx, "Verification failed", fe)
+ }
}
}
} catch {
diff --git a/src/test/scala/leon/test/LeonRegressionSuite.scala b/src/test/scala/leon/test/LeonRegressionSuite.scala
index 941cb9b90..58fdce2c6 100644
--- a/src/test/scala/leon/test/LeonRegressionSuite.scala
+++ b/src/test/scala/leon/test/LeonRegressionSuite.scala
@@ -33,7 +33,7 @@ trait LeonRegressionSuite extends FunSuite with Timeouts {
body
} catch {
case fe: LeonFatalError =>
- throw new TestFailedException("", fe, 5)
+ throw new TestFailedException("Uncaught LeonFatalError", fe, 5)
}
}
}
--
GitLab