diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-17 15:30:18 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-17 15:30:18 +0000 |
commit | 8b5bec4104a80d1be737d437c129922927b6945d (patch) | |
tree | 73c4d8fec3bdda31c219912c4d1cc7f9a83832dc /test-suite | |
parent | 0051054104b42fef484b6d309aebdae9ecd8bf0d (diff) |
Mise en place d'un test de correction de la sortie de commandes Coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2130 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
-rwxr-xr-x | test-suite/check | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/test-suite/check b/test-suite/check index f415604fd..f206c8413 100755 --- a/test-suite/check +++ b/test-suite/check @@ -40,8 +40,28 @@ test_echec() { done } +# La fonction suivante teste la sortie des fichiers qu'elle exécute +test_output() { + for f in $1/*.v; do + nbtests=`expr $nbtests + 1` + printf " "$f"..." + tmpoutput=`mktemp /tmp/coqcheck.XXXXXX` + $command $f | tail +3 > $tmpoutput 2>&1 + foutput=`dirname $f`/`basename $f .v`.out + diff $tmpoutput $foutput > /dev/null + if [ $? = 0 ]; then + echo "Ok" + nbtestsok=`expr $nbtestsok + 1` + else + echo "Error! (unexpected output)" + fi + done +} + # Programme principal +echo "Output tests" +test_output output echo "Success tests" test_succes success echo "Failure tests" |