From 5fe42a43b2e9ae1e9884efb51e3a0757135ec9a5 Mon Sep 17 00:00:00 2001
From: Marco Antognini <antognini.marco@gmail.com>
Date: Thu, 26 Nov 2015 19:09:18 +0100
Subject: [PATCH] Update GenC regression tests
---
.../regression/genc/valid/AbsArray.scala | 21 +++++++++++++++++++
.../genc/valid/ExpressionOrder.scala | 15 ++++++++++++-
src/test/scala/leon/genc/GenCSuite.scala | 2 +-
3 files changed, 36 insertions(+), 2 deletions(-)
create mode 100644 src/test/resources/regression/genc/valid/AbsArray.scala
diff --git a/src/test/resources/regression/genc/valid/AbsArray.scala b/src/test/resources/regression/genc/valid/AbsArray.scala
new file mode 100644
index 000000000..b3a592f1a
--- /dev/null
+++ b/src/test/resources/regression/genc/valid/AbsArray.scala
@@ -0,0 +1,21 @@
+import leon.lang._
+
+object AbsArray {
+ def abs(a: Array[Int]) {
+ var i = 0;
+ while (i < a.length) {
+ a(i) = if (a(i) < 0) -a(i) else a(i)
+ i = i + 1
+ }
+ }
+
+ def main = {
+ val a = Array(0, -1, 2, -3)
+
+ abs(a)
+
+ a(0) + a(1) - 1 + a(2) - 2 + a(3) - 3 // == 0
+ }
+}
+
+
diff --git a/src/test/resources/regression/genc/valid/ExpressionOrder.scala b/src/test/resources/regression/genc/valid/ExpressionOrder.scala
index 2969729a6..5507d8e19 100644
--- a/src/test/resources/regression/genc/valid/ExpressionOrder.scala
+++ b/src/test/resources/regression/genc/valid/ExpressionOrder.scala
@@ -41,7 +41,8 @@ object ExpressionOrder {
bool2int(test3(false), 8) +
bool2int(test4(false), 16) +
bool2int(test6, 32) +
- bool2int(test7, 64)
+ bool2int(test7, 64) +
+ bool2int(test8, 128)
def test0(b: Boolean) = {
val f = b && !b // == false
@@ -128,6 +129,18 @@ object ExpressionOrder {
c == 4
}
+ def test8 = {
+ var x = 0
+
+ def bar(y: Int) = {
+ def fun(z: Int) = 1 * x * (y + z)
+
+ fun(3)
+ }
+
+ bar(2) == 0
+ }
+
def bool2int(b: Boolean, f: Int) = if (b) 0 else f;
}
diff --git a/src/test/scala/leon/genc/GenCSuite.scala b/src/test/scala/leon/genc/GenCSuite.scala
index c63cbd9df..77405c6ef 100644
--- a/src/test/scala/leon/genc/GenCSuite.scala
+++ b/src/test/scala/leon/genc/GenCSuite.scala
@@ -87,7 +87,7 @@ class GenCSuite extends LeonRegressionSuite {
} catch {
case _: TimeoutException =>
p.destroy()
- p.exitValue()
+ throw LeonFatalError("timeout reached")
}
}
--
GitLab