From 1508a8e5e9d707fd302490d1c4aee35cda742ef2 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Thu, 7 Oct 2010 18:00:02 +0000
Subject: [PATCH] more new better
---
project/build/funcheck.scala | 9 ++++++---
src/funcheck/Annotations.scala | 5 +++++
src/funcheck/CodeExtraction.scala | 11 ++++++++++-
src/purescala/Definitions.scala | 10 +++++++++-
src/purescala/PrettyPrinter.scala | 7 ++++++-
src/purescala/Z3ModelReconstruction.scala | 14 ++++++++++++++
testcases/ListWithSize.scala | 4 +++-
7 files changed, 53 insertions(+), 7 deletions(-)
create mode 100644 src/funcheck/Annotations.scala
create mode 100644 src/purescala/Z3ModelReconstruction.scala
diff --git a/project/build/funcheck.scala b/project/build/funcheck.scala
index d4b148c4f..7c70f935d 100644
--- a/project/build/funcheck.scala
+++ b/project/build/funcheck.scala
@@ -30,20 +30,23 @@ class FunCheckProject(info: ProjectInfo) extends DefaultProject(info) with FileT
val f = scriptPath.asFile
val fw = new java.io.FileWriter(f)
fw.write("#!/bin/bash" + nl)
- fw.write("FUNCHECKCLASSPATH=")
+ fw.write("FUNCHECKCLASSPATH=\"")
fw.write(buildLibraryJar.absolutePath + ":")
fw.write(buildCompilerJar.absolutePath + ":")
fw.write(purescala.jarPath.absolutePath + ":")
fw.write(plugin.jarPath.absolutePath + ":")
fw.write(("lib" / "z3.jar").absolutePath)
- fw.write(nl + nl)
+ fw.write("\"" + nl + nl)
fw.write("for f in " + extensionJars.map(_.absolutePath).map(n => "\"" + n + "\"").mkString(" ") + "; do" + nl)
fw.write(" if [ -e ${f} ]" + nl)
fw.write(" then" + nl)
fw.write(" FUNCHECKCLASSPATH=${FUNCHECKCLASSPATH}:${f}" + nl)
fw.write(" fi" + nl)
fw.write("done" + nl + nl)
- fw.write("SCALACCLASSPATH=\"" + (multisetsLib.jarPath.absolutePath) + "\"" + nl)
+ fw.write("SCALACCLASSPATH=\"")
+ fw.write(multisetsLib.jarPath.absolutePath + ":")
+ fw.write(plugin.jarPath.absolutePath)
+ fw.write("\"" + nl + nl)
fw.write("LD_LIBRARY_PATH=" + ("." / "lib-bin").absolutePath + " \\" + nl)
fw.write("java \\" + nl)
diff --git a/src/funcheck/Annotations.scala b/src/funcheck/Annotations.scala
new file mode 100644
index 000000000..4d15717df
--- /dev/null
+++ b/src/funcheck/Annotations.scala
@@ -0,0 +1,5 @@
+package funcheck
+
+object Annotations {
+ class induct extends StaticAnnotation
+}
diff --git a/src/funcheck/CodeExtraction.scala b/src/funcheck/CodeExtraction.scala
index c6caa595e..e996e7bf8 100644
--- a/src/funcheck/CodeExtraction.scala
+++ b/src/funcheck/CodeExtraction.scala
@@ -155,7 +155,16 @@ trait CodeExtraction extends Extractors {
_ match {
case ExMainFunctionDef() => ;
case dd @ ExFunctionDef(n,p,t,b) => {
- defsToDefs += (dd.symbol -> extractFunSig(n, p, t))
+ val mods = dd.mods
+ val funDef = extractFunSig(n, p, t)
+ if(mods.isPrivate) funDef.addAnnotation("private")
+ for(a <- dd.symbol.annotations) {
+ a.atp.safeToString match {
+ case "funcheck.Annotations.induct" => funDef.addAnnotation("induct")
+ case _ => ;
+ }
+ }
+ defsToDefs += (dd.symbol -> funDef)
}
case _ => ;
}
diff --git a/src/purescala/Definitions.scala b/src/purescala/Definitions.scala
index 67fe9fd5b..9eaebe171 100644
--- a/src/purescala/Definitions.scala
+++ b/src/purescala/Definitions.scala
@@ -232,6 +232,14 @@ object Definitions {
def hasImplementation : Boolean = body.isDefined
def hasPrecondition : Boolean = precondition.isDefined
def hasPostcondition : Boolean = postcondition.isDefined
- }
+ private var annots: Set[String] = Set.empty[String]
+ def addAnnotation(as: String*) : FunDef = {
+ annots = annots ++ as
+ this
+ }
+ def annotations : Set[String] = annots
+
+ def isPrivate : Boolean = annots.contains("private")
+ }
}
diff --git a/src/purescala/PrettyPrinter.scala b/src/purescala/PrettyPrinter.scala
index 4b8207562..c073757ce 100644
--- a/src/purescala/PrettyPrinter.scala
+++ b/src/purescala/PrettyPrinter.scala
@@ -268,9 +268,14 @@ object PrettyPrinter {
nsb
}
- case FunDef(id, rt, args, body, pre, post) => {
+ case fd @ FunDef(id, rt, args, body, pre, post) => {
var nsb = sb
+ for(a <- fd.annotations) {
+ ind(nsb, lvl)
+ nsb.append("@" + a + "\n")
+ }
+
pre.foreach(prec => {
ind(nsb, lvl)
nsb.append("@pre : ")
diff --git a/src/purescala/Z3ModelReconstruction.scala b/src/purescala/Z3ModelReconstruction.scala
new file mode 100644
index 000000000..77688b217
--- /dev/null
+++ b/src/purescala/Z3ModelReconstruction.scala
@@ -0,0 +1,14 @@
+package purescala
+
+import z3.scala._
+import Common._
+import Definitions._
+import Extensions._
+import Trees._
+import TypeTrees._
+
+trait Z3ModelReconstruction {
+ self: Z3Solver =>
+
+
+}
diff --git a/testcases/ListWithSize.scala b/testcases/ListWithSize.scala
index b9425d804..130955bc6 100644
--- a/testcases/ListWithSize.scala
+++ b/testcases/ListWithSize.scala
@@ -1,4 +1,5 @@
import scala.collection.immutable.Set
+import funcheck.Annotations._
object ListWithSize {
sealed abstract class List
@@ -34,9 +35,10 @@ object ListWithSize {
case Cons(x,xs) => Cons(x, append(xs, l2))
})
+ @induct
def propAppend1(l : List) : Boolean = {
append(l, Nil()) == l
- }
+ } ensuring(_ == true)
def propAppend2(l : List) : Boolean = (l match {
case Nil() => propAppend1(l)
--
GitLab