3 # This script allows JPF to run on Benchexec.
4 # https://github.com/sosy-lab/benchexec
6 # create site.properties
7 SITE_PROPERTIES=site.properties
8 echo "jpf-core = `pwd`/jpf-core" > $SITE_PROPERTIES
9 echo "jpf-symbc = `pwd`/jpf-symbc" >> $SITE_PROPERTIES
10 echo "extensions=\${jpf-core},\${jpf-symbc}" >> $SITE_PROPERTIES
17 while [ -n "$1" ] ; do
19 --propertyfile) PROPERTY_FILE="$2" ; shift 2 ;;
20 --graphml-witness) WITNESS_FILE="$2" ; shift 2 ;;
21 --version) jpf-core/bin/jpf -version ; exit 0 ;;
22 *) BENCHMARK="$1" ; shift 1 ;;
26 if [ -z "$BENCHMARK" ] ; then
27 echo "Missing benchmark file"
31 if [ -z "$PROPERTY_FILE" ] ; then
32 echo "Missing property file"
36 if [ ! -s "$BENCHMARK" ] ; then
37 echo "Empty benchmark file"
41 if [ ! -s "$PROPERTY_FILE" ] ; then
42 echo "Empty property file"
46 LOG=`mktemp -t jpf-log.XXXXXX`
47 DIR=`mktemp -d -t jpf-benchmark.XXXXXX`
48 trap "rm -rf $DIR $LOG" EXIT
50 # we ignore the property file (there is only one property at the moment)
51 # we ignore the witness file (not used yet)
52 # we unpack the benchmark zip file, build it and analyze it
53 unzip $BENCHMARK -d $DIR
56 # create configuration file
57 echo "target=Main" > $DIR/config.jpf
58 echo "classpath=$DIR/target/classes" >> $DIR/config.jpf
59 echo "symbolic.dp=z3" >> $DIR/config.jpf
60 echo "listener = .symbc.SymbolicListener" >> $DIR/config.jpf
62 LD_LIBRARY_PATH=`pwd`/jpf-symbc/lib:$LD_LIBRARY_PATH
64 jpf-core/bin/jpf $DIR/config.jpf | tee $LOG
66 grep "no errors detected" $LOG > /dev/null
70 grep "^error.*NoUncaughtExceptionsProperty.*AssertionError" $LOG > /dev/null