examples/regtests.sh

   1 #!/bin/sh -eu
   2 # regression tests for why3
   3
   4 REPLAYOPT=""
   5 REGTESTS_MODE=""
   6
   7 while test $# != 0; do
   8 case "$1" in
   9   "--force")
  10         REPLAYOPT="$REPLAYOPT --force"
  11         ;;
  12   "--obsolete-only")
  13         REPLAYOPT="$REPLAYOPT --obsolete-only"
  14         ;;
  15   "--ignore-shapes")
  16         REPLAYOPT="$REPLAYOPT --ignore-shapes"
  17         ;;
  18   "--prover")
  19         REPLAYOPT="$REPLAYOPT --prover $2"
  20         shift
  21         ;;
  22   "--reduced-mode")
  23         REGTESTS_MODE="REDUCED"
  24         ;;
  25   *)
  26         echo "$0: Unknown option '$1'"
  27         exit 2
  28 esac
  29 shift
  30 done
  31
  32 TMP=$PWD/why3regtests.out
  33 TMPERR=$PWD/why3regtests.err
  34
  35 # Current directory is /examples
  36 cd `dirname $0`
  37
  38 # too early to do that
  39 # REPLAYOPT="$REPLAYOPT --smoke-detector top"
  40
  41 res=0
  42 export success=0
  43 export total=0
  44 export sessions=""
  45 export shapes=""
  46
  47
  48 run_dir () {
  49     if [ "$REGTESTS_MODE" = "REDUCED" ]; then
  50         if [ -f $1/reduced_regtests.list ]; then
  51             LIST=`sed $1/reduced_regtests.list -n -e "s&^\([^ #]\+\).*&$1/\1/why3session.xml&p"`
  52         else
  53             LIST=
  54         fi
  55     else
  56         LIST=`ls $1/*/why3session.xml`
  57     fi
  58     for f in $LIST; do
  59         d=`dirname $f`
  60         printf "Replaying $d ... "
  61         if ../bin/why3.opt replay -q $REPLAYOPT $2 $d 2> $TMPERR > $TMP ; then
  62             printf "OK"
  63             cat $TMP $TMPERR
  64             success=`expr $success + 1`
  65         else
  66             ret=$?
  67             printf "FAILED (ret code=$ret):"
  68             out=`head -1 $TMP`
  69             if test -z "$out" ; then
  70                echo "standard error: (standard output empty)"
  71                cat $TMPERR
  72             else
  73                cat $TMP
  74             fi
  75             res=1
  76         fi
  77         total=`expr $total + 1`
  78     done
  79     sessions="$sessions $1/*/why3session.xml"
  80     shapes="$shapes $1/*/why3shapes.gz"
  81 }
  82
  83 echo "=== Examples and Case Studies === MUST REPLAY AND ALL GOALS PROVED ==="
  84 echo ""
  85 run_dir . ""
  86 run_dir micro-c ""
  87 run_dir python ""
  88 run_dir double_wp "-L double_wp"
  89 run_dir avl "-L avl"
  90 run_dir c_cursor "-L c_cursor"
  91 run_dir foveoos11-cm ""
  92 run_dir vacid_0_binary_heaps "-L vacid_0_binary_heaps"
  93 run_dir verifythis_2016_matrix_multiplication "-L verifythis_2016_matrix_multiplication"
  94 run_dir WP_revisited ""
  95 run_dir prover "-L prover --warn-off=unused_variable"
  96 run_dir multiprecision "-L multiprecision"
  97 run_dir c_cursor "-L c_cursor"
  98 run_dir numeric ""
  99 echo ""
 100
 101 echo "Score on Examples and Case Studies: $success/$total"
 102 echo ""
 103
 104 echo "=== Standard Library ==="
 105 echo ""
 106 run_dir stdlib ""
 107 echo ""
 108
 109 echo "=== Tests ==="
 110 echo ""
 111 # there's no session there...
 112 # run_dir tests
 113 run_dir tests-provers ""
 114 echo ""
 115
 116 echo "=== Check Builtin translation ==="
 117 echo ""
 118 run_dir check-builtin ""
 119 echo ""
 120
 121 echo "=== BTS ==="
 122 echo ""
 123 run_dir bts ""
 124 echo ""
 125
 126 echo "=== Logic ==="
 127 echo ""
 128 run_dir logic ""
 129 run_dir bitvectors "-L bitvectors"
 130 echo ""
 131
 132 echo "=== MLCFG ==="
 133 echo ""
 134 run_dir mlcfg ""
 135 echo ""
 136
 137 echo "Summary       : $success/$total"
 138 echo "Sessions size : "`wc -cl $sessions | tail -1`
 139 echo "Shapes   size : "`wc -cl $shapes | tail -1`
 140
 141 exit $res