bin/jpf-sv-comp

   1 #!/bin/bash
   2
   3 # This script allows JPF to run on Benchexec.
   4 # https://github.com/sosy-lab/benchexec
   5
   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
  11
  12 # parse arguments
  13 BENCHMARK=""
  14 PROPERTY_FILE=""
  15 WITNESS_FILE=""
  16
  17 while [ -n "$1" ] ; do
  18   case "$1" in
  19     --propertyfile) PROPERTY_FILE="$2" ; shift 2 ;;
  20     --graphml-witness) WITNESS_FILE="$2" ; shift 2 ;;
  21     --version) bin/jpf -version ; exit 0 ;;
  22     *) BENCHMARK="$1" ; shift 1 ;;
  23   esac
  24 done
  25
  26 if [ -z "$BENCHMARK" ] ; then
  27   echo "Missing benchmark file"
  28   exit 1
  29 fi
  30
  31 if [ -z "$PROPERTY_FILE" ] ; then
  32   echo "Missing property file"
  33   exit 1
  34 fi
  35
  36 if [ ! -s "$BENCHMARK" ]  ; then
  37   echo "Empty benchmark file"
  38   exit 1
  39 fi
  40
  41 if [ ! -s "$PROPERTY_FILE" ] ; then
  42   echo "Empty property file"
  43   exit 1
  44 fi
  45
  46 LOG=`mktemp -t jpf-log.XXXXXX`
  47 DIR=`mktemp -d -t jpf-benchmark.XXXXXX`
  48 trap "rm -rf $DIR $LOG" EXIT
  49
  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
  54 make -C $DIR
  55
  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
  61
  62 LD_LIBRARY_PATH=`pwd`/jpf-symbc/lib:$LD_LIBRARY_PATH
  63
  64 bin/jpf $DIR/config.jpf | tee $LOG
  65
  66 grep "no errors detected" $LOG > /dev/null
  67 if [ $? -eq 0 ]; then
  68   echo "SAFE"
  69 else
  70   grep "^error.*NoUncaughtExceptionsProperty.*AssertionError" $LOG > /dev/null
  71   if [ $? -eq 0 ]; then
  72     echo "UNSAFE"
  73   else
  74     echo "UNKNOWN"
  75   fi
  76 fi