initial commit

Readme

@@ -0,0 +1,24 @@
+Symbolic (Java) PathFinder:
+---------------------------
+
+Created new branch that contains many updates to SPF;
+in particular, interfacing with Z3 is robust; 
+also SPF now has a "symcrete" mode that executes paths 
+triggered by concrete inputs and collects constraints along the paths
+
+This JPF extension provides symbolic execution for Java bytecode.
+It performs a non-standard interpretation of byte-codes.
+Currently, it allows symbolic execution on methods with arguments of basic types
+(int, long, double, boolean, etc.). Symbolic input globals and method
+pre-conditions are specified via user annotations (see symbc/examples and
+symbc/test).
+
+A paper describing Symbolic PathFinder appeared at ISSTA'08:
+
+Title: Combining Unit-level Symbolic Execution and System-level Concrete
+Execution for Testing NASA Software,
+Authors: C. S. Pasareanu, P. C. Mehlitz, D. H. Bushnell, K. Gundy-Burlet,
+M. Lowry, S. Person, M. Pape.
+
+Tool documentation can be found at:
+http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-symbc

ReadmeMultipleDecisionProcedures

@@ -0,0 +1,43 @@
+Support for multiple decision procedures (based on work done by Saswat 
+Anand for old symbolic framework);
+set the "symbolic.dp" JPF configuration variable to one of the modes below.
+I don't intend to keep the old file,pipe interface.
+We will support: CVC3/CVCLite, STP, Yices, Omega.
+
+For example from command line you can use "+symbolic.dp=omega.native", 
+in which case JPF will use omega native interface.
+
+Supported modes:
+omega.native
+omega.native.inc
+yices.native
+yices.native.inc
+yices.native.incsolve
+cvcl.native
+cvcl.native.inc
+cvcl.native.incsolve
+stp.native
+
+Description of Modes:
+<name>.native - JNI Interface for decision procedure <name> 
+	Path conditions are maintained inside JPF world.
+	No problems with printing. Solving is done by POOC.	
+
+<name>.native.inc - Path conditions are maintained in C side.
+	Checking of constraint is done incrementally.
+	Printing and solving does not work yet. Easy to fix.
+
+<name>.native.incsolve - Constraints are checked incrementally
+	using push/pop feature of decision procedures. Not 
+	clear on how to print/solve path condition.
+
+
+Notes:
+1. Subsumption works only for omega.native correctly. (not sure if I'll keep 
+this).
+2. omega.inc and yice.native.incsolve are usually the fastest.
+3. Reals: yices.native.* and cvcl.native.* handle real linear constraints.
+
+
+
+

bin/ant

@@ -0,0 +1,12 @@
+#!/bin/bash
+#
+# unix shell script to run ant through RunAnt.jar
+#
+
+JPF_HOME=`dirname "$0"`/..
+
+if test -z "$JVM_FLAGS"; then
+  JVM_FLAGS="-Xmx1024m -ea"
+fi
+
+java $JVM_FLAGS -jar "$JPF_HOME/tools/RunAnt.jar" "$@"

bin/ant.bat

@@ -0,0 +1,12 @@
+REM
+REM overly simplified batch file to start Ant through RunAnt.jar from a command prompt
+REM
+
+@echo off
+
+REM Set the JPF_HOME directory
+set JPF_HOME=%~dp0..
+
+set JVM_FLAGS=-Xmx1024m -ea
+
+java %JVM_FLAGS% -jar "%JPF_HOME%\tools\RunAnt.jar" %*

bin/jpf

@@ -0,0 +1,12 @@
+#!/bin/bash
+#
+# unix shell script to run jpf
+#
+
+JPF_HOME=`dirname "$0"`/..
+
+if test -z "$JVM_FLAGS"; then
+  JVM_FLAGS="-Xmx1024m -ea"
+fi
+
+java $JVM_FLAGS -jar "$JPF_HOME/tools/RunJPF.jar" "$@"

bin/jpf.bat

@@ -0,0 +1,13 @@
+REM
+REM overly simplified batch file to start JPF from a command prompt
+REM
+
+@echo off
+
+REM Set the JPF_HOME directory
+set JPF_HOME=%~dp0..
+
+set JVM_FLAGS=-Xmx1024m -ea
+
+java %JVM_FLAGS% -jar "%JPF_HOME%\tools\RunJPF.jar" %*
+

bin/test

@@ -0,0 +1,13 @@
+#!/bin/bash
+#
+# unix shell script to run jpf
+#
+
+JPF_HOME=`dirname "$0"`/..
+
+if test -z "$JVM_FLAGS"; then
+  JVM_FLAGS="-Xmx1024m -ea"
+fi
+
+java $JVM_FLAGS -jar "$JPF_HOME/tools/RunTest.jar" "$@"
+