bench/coma

   1 #!/bin/bash
   2
   3 pgm="bin/why3 prove"
   4
   5 coma_bad () {
   6     test -d $1 || exit 1
   7     for f in $1/*.coma ; do
   8         printf "  $f... "
   9         if $pgm $2 $f > /dev/null 2>&1; then
  10             echo "failed! (should have an error)"
  11             echo $pgm $2 $f
  12             $pgm $2 $f
  13             exit 1
  14         fi
  15         echo "ok"
  16     done
  17 }
  18
  19 coma_good () {
  20     test -d $1 || exit 1
  21     rm -f bench_errors
  22     rm -f bench_error
  23     for f in $1/*.$2 ; do
  24         printf "  $f... "
  25         if ! $pgm $f > /dev/null 2> bench_error; then
  26             echo "failed!"
  27             echo "invocation: $pgm $opts $f" | tee -a bench_errors
  28             cat bench_error | tee -a bench_errors
  29             rm -f bench_errors bench_error
  30             exit 1
  31         fi
  32         rm -f bench_error
  33         echo "ok"
  34     done
  35 }
  36
  37 simple_test() {
  38     if ! "$@" > /dev/null 2> /dev/null; then
  39         echo "failed!"
  40         echo "$@"
  41         "$@"
  42         exit 1
  43     fi
  44     echo "ok"
  45 }
  46
  47 replay () {
  48     pgm="bin/why3 replay"
  49     test -d $1 || exit 1
  50     for f in $1/*/; do
  51         printf "  $f... "
  52         simple_test $pgm $f
  53     done
  54 }
  55
  56 make -j
  57
  58 echo "=== Checking bad files (Coma) ==="
  59 coma_bad ./bench/plugins/coma/bad
  60 echo ""
  61
  62 echo "=== Checking good files (Coma) ==="
  63 coma_good ./examples/coma coma
  64 coma_good ./bench/plugins/coma/good coma
  65 echo ""
  66
  67 echo "=== Checking replay (Coma) ==="
  68 replay ./examples/coma
  69 echo ""