From 30e4b8ac7490a57390b62d5bf1530a98446f931a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Mon, 7 May 2012 23:59:40 +0000
Subject: [PATCH] basic infrastructure to generate test cases
---
src/main/scala/leon/Extensions.scala | 1 +
src/main/scala/leon/purescala/Trees.scala | 12 ++++++
testcases/Abs.scala | 48 +--------------------
testcases/AbsArray.scala | 51 +++++++++++++++++++++++
4 files changed, 65 insertions(+), 47 deletions(-)
create mode 100644 testcases/AbsArray.scala
diff --git a/src/main/scala/leon/Extensions.scala b/src/main/scala/leon/Extensions.scala
index 5905ec998..7d8469998 100644
--- a/src/main/scala/leon/Extensions.scala
+++ b/src/main/scala/leon/Extensions.scala
@@ -98,6 +98,7 @@ object Extensions {
allLoaded = defaultExtensions ++ loaded
analysisExtensions = allLoaded.filter(_.isInstanceOf[Analyser]).map(_.asInstanceOf[Analyser])
+ analysisExtensions = new TestGeneration(extensionsReporter) +: analysisExtensions
val solverExtensions0 = allLoaded.filter(_.isInstanceOf[Solver]).map(_.asInstanceOf[Solver])
val solverExtensions1 = if(Settings.useQuickCheck) new RandomSolver(extensionsReporter) +: solverExtensions0 else solverExtensions0
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 638db0c20..ee3daffb7 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -842,6 +842,18 @@ object Trees {
}
treeCatamorphism(convert, combine, compute, expr)
}
+ def containsIfExpr(expr: Expr): Boolean = {
+ def convert(t : Expr) : Boolean = t match {
+ case (i: IfExpr) => true
+ case _ => false
+ }
+ def combine(c1 : Boolean, c2 : Boolean) : Boolean = c1 || c2
+ def compute(t : Expr, c : Boolean) = t match {
+ case (i: IfExpr) => true
+ case _ => c
+ }
+ treeCatamorphism(convert, combine, compute, expr)
+ }
def variablesOf(expr: Expr) : Set[Identifier] = {
def convert(t: Expr) : Set[Identifier] = t match {
diff --git a/testcases/Abs.scala b/testcases/Abs.scala
index 5efb41797..52baf7101 100644
--- a/testcases/Abs.scala
+++ b/testcases/Abs.scala
@@ -1,51 +1,5 @@
-import leon.Utils._
-
object Abs {
-
- def abs(tab: Map[Int, Int], size: Int): Map[Int, Int] = ({
- require(size <= 5 && isArray(tab, size))
- var k = 0
- var tabres = Map.empty[Int, Int]
- (while(k < size) {
- if(tab(k) < 0)
- tabres = tabres.updated(k, -tab(k))
- else
- tabres = tabres.updated(k, tab(k))
- k = k + 1
- }) invariant(isArray(tabres, k) && k >= 0 && k <= size && isPositive(tabres, k))
- tabres
- }) ensuring(res => isArray(res, size) && isPositive(res, size))
-
- def isPositive(a: Map[Int, Int], size: Int): Boolean = {
- require(size <= 10 && isArray(a, size))
- def rec(i: Int): Boolean = {
- require(i >= 0)
- if(i >= size)
- true
- else {
- if(a(i) < 0)
- false
- else
- rec(i+1)
- }
- }
- rec(0)
- }
-
- def isArray(a: Map[Int, Int], size: Int): Boolean = {
-
- def rec(i: Int): Boolean = {
- require(i >= 0)
- if(i >= size) true else {
- if(a.isDefinedAt(i)) rec(i+1) else false
- }
- }
-
- if(size < 0)
- false
- else
- rec(0)
- }
+ def abs(x: Int): Int = (if(x < 0) -x else x) ensuring(_ >= 0)
}
diff --git a/testcases/AbsArray.scala b/testcases/AbsArray.scala
new file mode 100644
index 000000000..0086891cd
--- /dev/null
+++ b/testcases/AbsArray.scala
@@ -0,0 +1,51 @@
+import leon.Utils._
+
+object AbsArray {
+
+
+ def abs(tab: Map[Int, Int], size: Int): Map[Int, Int] = ({
+ require(size <= 5 && isArray(tab, size))
+ var k = 0
+ var tabres = Map.empty[Int, Int]
+ (while(k < size) {
+ if(tab(k) < 0)
+ tabres = tabres.updated(k, -tab(k))
+ else
+ tabres = tabres.updated(k, tab(k))
+ k = k + 1
+ }) invariant(isArray(tabres, k) && k >= 0 && k <= size && isPositive(tabres, k))
+ tabres
+ }) ensuring(res => isArray(res, size) && isPositive(res, size))
+
+ def isPositive(a: Map[Int, Int], size: Int): Boolean = {
+ require(size <= 10 && isArray(a, size))
+ def rec(i: Int): Boolean = {
+ require(i >= 0)
+ if(i >= size)
+ true
+ else {
+ if(a(i) < 0)
+ false
+ else
+ rec(i+1)
+ }
+ }
+ rec(0)
+ }
+
+ def isArray(a: Map[Int, Int], size: Int): Boolean = {
+
+ def rec(i: Int): Boolean = {
+ require(i >= 0)
+ if(i >= size) true else {
+ if(a.isDefinedAt(i)) rec(i+1) else false
+ }
+ }
+
+ if(size < 0)
+ false
+ else
+ rec(0)
+ }
+
+}
--
GitLab