From 1dd91cc0775b58ef1a3d6d72eed92070c0a3c029 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ali=20Sinan=20K=C3=B6ksal?= <alisinan@gmail.com>
Date: Wed, 19 Jan 2011 16:25:06 +0000
Subject: [PATCH] Test integer lower and upper bounds specified as command-line
option.
---
src/funcheck/FunCheckPlugin.scala | 2 ++
src/purescala/Settings.scala | 1 +
src/purescala/Z3Solver.scala | 4 ++--
3 files changed, 5 insertions(+), 2 deletions(-)
diff --git a/src/funcheck/FunCheckPlugin.scala b/src/funcheck/FunCheckPlugin.scala
index 89af09e58..9337fb700 100644
--- a/src/funcheck/FunCheckPlugin.scala
+++ b/src/funcheck/FunCheckPlugin.scala
@@ -29,6 +29,7 @@ class FunCheckPlugin(val global: Global) extends Plugin {
" -P:funcheck:nobapa Disable BAPA Z3 extension" + "\n" +
" -P:funcheck:impure Generate testcases only for impure functions" + "\n" +
" -P:funcheck:testcases=[1,2] Number of testcases to generate per function" + "\n" +
+ " -P:funcheck:testbounds=l:u Lower and upper bounds for integers in recursive datatypes" + "\n" +
" -P:funcheck:quiet No info and warning messages from the extensions" + "\n" +
" -P:funcheck:XP Enable weird transformations and other bug-producing features" + "\n" +
" -P:funcheck:PLDI PLDI 2011 settings. Now frozen. Not completely functional. See CAV." + "\n" +
@@ -56,6 +57,7 @@ class FunCheckPlugin(val global: Global) extends Plugin {
case s if s.startsWith("unrolling=") => purescala.Settings.unrollingLevel = try { s.substring("unrolling=".length, s.length).toInt } catch { case _ => 0 }
case s if s.startsWith("functions=") => purescala.Settings.functionsToAnalyse = Set(splitList(s.substring("functions=".length, s.length)): _*)
case s if s.startsWith("extensions=") => purescala.Settings.extensionNames = splitList(s.substring("extensions=".length, s.length))
+ case s if s.startsWith("testbounds=") => purescala.Settings.testBounds = try { val l = splitList(s.substring("testBounds=".length, s.length)).map(_.toInt); if (l.size != 2) (0, 3) else (l(0), l(1)) } catch { case _ => (0, 3) }
case s if s.startsWith("testcases=") => purescala.Settings.nbTestcases = try { s.substring("testcases=".length, s.length).toInt } catch { case _ => 1 }
case _ => error("Invalid option: " + option)
}
diff --git a/src/purescala/Settings.scala b/src/purescala/Settings.scala
index 720b3ea58..c1e378783 100644
--- a/src/purescala/Settings.scala
+++ b/src/purescala/Settings.scala
@@ -16,6 +16,7 @@ object Settings {
var useBAPA: Boolean = true
var impureTestcases: Boolean = false
var nbTestcases: Int = 1
+ var testBounds: (Int, Int) = (0, 3)
var useInstantiator: Boolean = false
var useFairInstantiator: Boolean = false
def useAnyInstantiator : Boolean = useInstantiator || useFairInstantiator
diff --git a/src/purescala/Z3Solver.scala b/src/purescala/Z3Solver.scala
index aad4a92a0..30585f288 100644
--- a/src/purescala/Z3Solver.scala
+++ b/src/purescala/Z3Solver.scala
@@ -176,8 +176,8 @@ class Z3Solver(val reporter: Reporter) extends Solver(reporter) with AbstractZ3S
}
private def boundValues : Unit = {
- val upperBound: Z3AST = z3.mkInt(3, z3.mkIntSort)
- val lowerBound: Z3AST = z3.mkInt(0, z3.mkIntSort)
+ val lowerBound: Z3AST = z3.mkInt(Settings.testBounds._1, z3.mkIntSort)
+ val upperBound: Z3AST = z3.mkInt(Settings.testBounds._2, z3.mkIntSort)
def isUnbounded(field: VarDecl) : Boolean = field.getType match {
case Int32Type => true
--
GitLab