From bd79adf73f8a38907dbf1a40d480d8d2c11671ca Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Mon, 5 Mar 2012 16:47:41 +0100
Subject: [PATCH] more cleaning up
---
README | 1 -
WISHLIST | 26 --------------------------
funcheck-laraserver | 15 ---------------
3 files changed, 42 deletions(-)
delete mode 100644 README
delete mode 100644 WISHLIST
delete mode 100755 funcheck-laraserver
diff --git a/README b/README
deleted file mode 100644
index c77e299e9..000000000
--- a/README
+++ /dev/null
@@ -1 +0,0 @@
-Trying to clean the slate.
diff --git a/WISHLIST b/WISHLIST
deleted file mode 100644
index e559aff38..000000000
--- a/WISHLIST
+++ /dev/null
@@ -1,26 +0,0 @@
-Do Add here what you would love FunCheck to be able to do
-------------------------------------------------------
-VK: support maps Map[A,B] for ground types A,B (no polymorphism)
-VK: add bitvectors, including multiplication of int32 variables
-
-PS: support multiple top-level objects
-PS: support tuples (including natively in Z3)
-PS: implement @induct tactic, completely, not just for one arg
-PS: construct models for sets properly (also in interpreter)
-PS: support maps natively
-
-PS: use different levels of summaries (eg. just contract, part of contract
-that's public, then finally body) in unrollings, trying to minimize the
-branching at first
-
-Wishes granted so far
----------------------
-
-PS: create a wishlist
-PS: rewrite pattern-matching translator to use if-then-else
-VK: add IsValid class to allow for writing just "holds" in place of ensuring(_ == true)
-PS: generate VCs for preconditions
-PS: generate VCs for pattern-matching
-PS: use 'private' accessor to indicate what's part of the interface
-PS: use a theory plugin to instantiate/unroll function bodies
-PS: instantiate/unroll function bodies in a fair way, to guarantee termination
diff --git a/funcheck-laraserver b/funcheck-laraserver
deleted file mode 100755
index 418bf2959..000000000
--- a/funcheck-laraserver
+++ /dev/null
@@ -1,15 +0,0 @@
-#!/bin/bash
-FUNCHECKCLASSPATH="/localhome/liftweb/funcheck/project/boot/scala-2.8.1/lib/scala-library.jar:/localhome/liftweb/funcheck/project/boot/scala-2.8.1/lib/scala-compiler.jar:/localhome/liftweb/funcheck/bin/purescala/purescala-definitions_2.8.1-1.0.jar:/localhome/liftweb/funcheck/bin/funcheck/funcheck-plugin_2.8.1-1.0.jar:/localhome/liftweb/funcheck/lib/z3.jar"
-
-for f in "/localhome/liftweb/funcheck/bin/multisets-lib/multiset-placeholder-library_2.8.1-1.0.jar" "/localhome/liftweb/funcheck/bin/multisets/multiset-solver_2.8.1-1.0.jar" "/localhome/liftweb/funcheck/bin/orderedsets/ordered-sets-solver_2.8.1-1.0.jar" "/localhome/liftweb/funcheck/bin/setconstraints/type-inference-with-set-constraints_2.8.1-1.0.jar"; do
- if [ -e ${f} ]
- then
- FUNCHECKCLASSPATH=${FUNCHECKCLASSPATH}:${f}
- fi
-done
-
-SCALACCLASSPATH="/localhome/liftweb/funcheck/bin/multisets-lib/multiset-placeholder-library_2.8.1-1.0.jar:/localhome/liftweb/funcheck/bin/funcheck/funcheck-plugin_2.8.1-1.0.jar:/localhome/liftweb/funcheck/bin/purescala/purescala-definitions_2.8.1-1.0.jar"
-
-LD_LIBRARY_PATH=/localhome/liftweb/libstdc++:/localhome/liftweb/z3/z3-2.19/lib \
-scala -classpath ${FUNCHECKCLASSPATH}:${SCALACCLASSPATH} \
-funcheck.Main -cp /localhome/liftweb/funcheck/bin/funcheck/funcheck-plugin_2.8.1-1.0.jar $@
--
GitLab