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 "extensions=\${jpf-core}" >> $SITE_PROPERTIES
16 while [ -n "$1" ] ; do
18 --propertyfile) PROPERTY_FILE="$2" ; shift 2 ;;
19 --graphml-witness) WITNESS_FILE="$2" ; shift 2 ;;
20 --version) jpf-core/bin/jpf -version ; exit 0 ;;
21 *) BENCHMARK="$1" ; shift 1 ;;
25 if [ -z "$BENCHMARK" ] ; then
26 echo "Missing benchmark file"
30 if [ -z "$PROPERTY_FILE" ] ; then
31 echo "Missing property file"
35 if [ ! -s "$BENCHMARK" ] ; then
36 echo "Empty benchmark file"
40 if [ ! -s "$PROPERTY_FILE" ] ; then
41 echo "Empty property file"
45 LOG=`mktemp -t jpf-log.XXXXXX`
46 DIR=`mktemp -d -t jpf-benchmark.XXXXXX`
47 trap "rm -rf $DIR $LOG" EXIT
49 # we ignore the property file (there is only one property at the moment)
50 # we ignore the witness file (not used yet)
51 # we unpack the benchmark zip file, build it and analyze it
52 unzip $BENCHMARK -d $DIR
55 # create configuration file
56 echo "target=Main" > $DIR/config.jpf
57 echo "classpath=$DIR/target/classes" >> $DIR/config.jpf
58 echo "cg.enumerate_random=true" >> $DIR/config.jpf
60 LD_LIBRARY_PATH=`pwd`/jpf-symbc/lib:$LD_LIBRARY_PATH
62 jpf-core/bin/jpf $DIR/config.jpf +cg.enumerate_random | tee $LOG
64 grep "no errors detected" $LOG > /dev/null
68 grep "^error.*NoUncaughtExceptionsProperty.*AssertionError" $LOG > /dev/null