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