diff options
Diffstat (limited to 'test')
| -rwxr-xr-x | test/coq/run_tests.sh | 12 | ||||
| -rw-r--r-- | test/coq/skip | 4 |
2 files changed, 13 insertions, 3 deletions
diff --git a/test/coq/run_tests.sh b/test/coq/run_tests.sh index da6bce69..c31b1475 100755 --- a/test/coq/run_tests.sh +++ b/test/coq/run_tests.sh @@ -5,7 +5,13 @@ DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" SAILDIR="$DIR/../.." TYPECHECKTESTSDIR="$DIR/../typecheck/pass" EXTRATESTSDIR="$DIR/pass" -BBVDIR="$DIR/../../../bbv/src/bbv" + +if [ -z "$BBVDIR" ] || opam config var coq-bbv:share >/dev/null 2>/dev/null; then + COQOPTS="-Q $SAILDIR/lib/coq Sail" +else + BBVDIR="$DIR/../../../bbv/src/bbv" + COQOPTS="-Q $SAILDIR/lib/coq Sail -Q $BBVDIR bbv" +fi RED='\033[0;31m' GREEN='\033[0;32m' @@ -56,8 +62,8 @@ function check_tests_dir { do if $SAILDIR/sail -coq -dcoq_undef_axioms -o out $TESTSDIR/$i &>/dev/null; then - if coqc -R "$BBVDIR" bbv -R "$SAILDIR/lib/coq" Sail out_types.v &>/dev/null && - coqc -R "$BBVDIR" bbv -R "$SAILDIR/lib/coq" Sail out.v &>/dev/null; + if coqc $COQOPTS out_types.v &>/dev/null && + coqc $COQOPTS out.v &>/dev/null; then green "tested $i expecting pass" "pass" else diff --git a/test/coq/skip b/test/coq/skip index b99c87ad..7a233ddc 100644 --- a/test/coq/skip +++ b/test/coq/skip @@ -35,5 +35,9 @@ while_MM.sail while_MP.sail while_PM.sail while_PP.sail +XXXXX Non-terminating loop that's only really useful for the type checking tests +repeat_constraint.sail XXXXX Not yet - haven't decided whether to support register reads in measures while_MM_terminating.sail +XXXXX TODO, add termination measure +floor_pow2.sail |