Readme

src/examples/Example.java

@@ -0,0 +1,48 @@
+/*
+ * Copyright (C)  2022  Franck van Breugel
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+/**
+ * A simple example.
+ * 
+ * @author Franck van Breugel
+ */
+public class Example {
+
+	/**
+	 * Returns the minimum of the given integers. 
+	 * 
+	 * @param x an integer
+	 * @param y an integer
+	 * @return the minimum of x and y
+	 */
+	private static int min(int x, int y) {
+		if (x > y) {
+			// swap x and y
+			x = x + y;
+			y = x - y;
+			x = x - y;
+		}
+		if (x > y) {
+			assert false;
+		}
+		return x;
+	}
+
+	public static void main(String[] args) {
+		Example.min(0, 1);
+	}
+}

src/examples/ExampleCVC3.jpf

@@ -0,0 +1,55 @@
+# Before running this example, link dynamic/shared library files for CVC3
+#
+# Windows (64-bit)
+# The dynamic library files for CVC3 for Windows 64-bit machines are not readily available.  
+# As a result, this example cannot be run on Windows 64-bit machines.
+#
+# Linux (64-bit)
+# To link the 64-bit shared library files, add the path /path/to/lib/64bit/subdirectory/of/jpf-symbc/
+# to the LD_LIBRARY_PATH environment variable.  For example, in a Linux sh issue the following command.
+#   export LD_LIBRARY_PATH=/path/to/lib/64bit/subdirectory/of/jpf-symbc/
+# In a Linux csh issue the following command.
+#   setenv LD_LIBRARY_PATH /path/to/lib/64bit/subdirectory/of/jpf-symbc/
+#
+# macOS (64-bit)
+# To link the 64-bit shared library files, add the path /path/to/lib/64bit/subdirectory/of/jpf-symbc/
+# to the DYLD_LIBRARY_PATH environment variable.  For example, in a Linux sh issue the following command.
+#   export DYLD_LIBRARY_PATH=/path/to/lib/64bit/subdirectory/of/jpf-symbc/
+# In a Linux csh issue the following command.
+#   setenv DYLD_LIBRARY_PATH /path/to/lib/64bit/subdirectory/of/jpf-symbc/
+#
+# Windows (32-bit)
+# To link the 32-bit dynamic library files, add the path /path/to/lib/subdirectory/of/jpf-symbc/
+# to the PATH environment variable.
+#
+# Linux (32-bit)
+# To link the 32-bit shared library files, add the path /path/to/lib/subdirectory/of/jpf-symbc/
+# to the LD_LIBRARY_PATH environment variable.  For example, in a Linux sh issue the following command.
+#   export LD_LIBRARY_PATH=/path/to/lib/subdirectory/of/jpf-symbc/
+# In a Linux csh issue the following command.
+#   setenv LD_LIBRARY_PATH /path/to/lib/subdirectory/of/jpf-symbc/
+#
+# macOS (32-bit)
+# To link the 32-bit shared library files, add the path /path/to/lib/subdirectory/of/jpf-symbc/
+# to the DYLD_LIBRARY_PATH environment variable.  For example, in a Linux sh issue the following command.
+#   export DYLD_LIBRARY_PATH=/path/to/lib/subdirectory/of/jpf-symbc/
+# In a Linux csh issue the following command.
+#   setenv DYLD_LIBRARY_PATH /path/to/lib/subdirectory/of/jpf-symbc/
+
+# fully qualified name of the Java app
+target = Example
+
+# path to the bytecode of the target (and classes used by the target)
+classpath = ${jpf-symbc}/build/examples
+
+# path to the Java code of the target (and classes used by the target)
+sourcepath = ${jpf-symbc}/src/examples
+
+# method and its parameters
+symbolic.method = Example.min(sym#sym)
+
+# solver used
+symbolic.dp = cvc3
+
+# listener that generates JUnit test cases
+listener = gov.nasa.jpf.symbc.sequences.SymbolicSequenceListener

src/examples/ExampleChoco.jpf

@@ -0,0 +1,17 @@
+# fully qualified name of the Java app
+target = Example
+
+# path to the bytecode of the target (and classes used by the target)
+classpath = ${jpf-symbc}/build/examples
+
+# path to the Java code of the target (and classes used by the target)
+sourcepath = ${jpf-symbc}/src/examples
+
+# method and its parameters
+symbolic.method = Example.min(sym#sym)
+
+# solver used (default)
+symbolic.dp = choco
+
+# listener that generates JUnit test cases
+listener = gov.nasa.jpf.symbc.sequences.SymbolicSequenceListener

src/examples/ExampleCoral.jpf

@@ -0,0 +1,17 @@
+# fully qualified name of the Java app
+target = Example
+
+# path to the bytecode of the target (and classes used by the target)
+classpath = ${jpf-symbc}/build/examples
+
+# path to the Java code of the target (and classes used by the target)
+sourcepath = ${jpf-symbc}/src/examples
+
+# method and its parameters
+symbolic.method = Example.min(sym#sym)
+
+# solver used
+symbolic.dp = coral
+
+# listener that generates JUnit test cases
+listener = gov.nasa.jpf.symbc.sequences.SymbolicSequenceListener

src/examples/ExampleIASolver.jpf

@@ -0,0 +1,17 @@
+# fully qualified name of the Java app
+target = Example
+
+# path to the bytecode of the target (and classes used by the target)
+classpath = ${jpf-symbc}/build/examples
+
+# path to the Java code of the target (and classes used by the target)
+sourcepath = ${jpf-symbc}/src/examples
+
+# method and its parameters
+symbolic.method = Example.min(sym#sym)
+
+# solver used
+symbolic.dp = iasolver
+
+# listener that generates JUnit test cases
+listener = gov.nasa.jpf.symbc.sequences.SymbolicSequenceListener

src/examples/ExampleZ3.jpf

@@ -0,0 +1,38 @@
+# Before running this example, link dynamic/shared library files for Z3
+#
+# Windows (64-bit)
+# To link the dynamic library files, add the path /path/to/lib/subdirectory/of/jpf-symbc/
+# to the PATH environment variable.  For example, in a Windows 10 PowerShell issue following command.
+#   $Env:PATH = "/path/to/lib/subdirectory/of/jpf-symbc/;" + $Env:PATH
+#
+# Linux (64-bit)
+# To link the shared library files, add the path /path/to/lib/subdirectory/of/jpf-symbc/
+# to the LD_LIBRARY_PATH environment variable.  For example, in a Linux sh issue the following command.
+#   export LD_LIBRARY_PATH=/path/to/lib/subdirectory/of/jpf-symbc/
+# In a Linux csh issue the following command.
+#   setenv LD_LIBRARY_PATH /path/to/lib/subdirectory/of/jpf-symbc/
+#
+# macOS (64-bit)
+# To link the shared library files, add the path /path/to/lib/subdirectory/of/jpf-symbc/
+# to the DYLD_LIBRARY_PATH environment variable.  For example, in a Linux sh issue the following command.
+#   export DYLD_LIBRARY_PATH=/path/to/lib/subdirectory/of/jpf-symbc/
+# In a Linux csh issue the following command.
+#   setenv DYLD_LIBRARY_PATH /path/to/lib/subdirectory/of/jpf-symbc/
+
+# fully qualified name of the Java app
+target = Example
+
+# path to the bytecode of the target (and classes used by the target)
+classpath = ${jpf-symbc}/build/examples
+
+# path to the Java code of the target (and classes used by the target)
+sourcepath = ${jpf-symbc}/src/examples
+
+# method and its parameters
+symbolic.method = Example.min(sym#sym)
+
+# solver used
+symbolic.dp = z3
+
+# listener that generates JUnit test cases
+listener = gov.nasa.jpf.symbc.sequences.SymbolicSequenceListener