This is an automated email from the git hooks/post-receive script.
treinen pushed a commit to branch master
in repository why.
commit 355dcfe56fecc58e106ce3af6b4adaf3996592ad
Author: Ralf Treinen <trei...@free.fr>
Date: Thu Oct 16 22:08:13 2014 +0200
improve as installed package tests
---
debian/changelog | 6 ++++++
debian/tests/control | 12 ++++--------
debian/tests/frama-c+jessie+alt-ergo | 19 ++++++++++---------
debian/tests/why+alt-ergo | 13 +++++--------
debian/tests/why+coq | 7 ++++---
debian/tests/why+cvc3 | 13 +++++--------
6 files changed, 34 insertions(+), 36 deletions(-)
diff --git a/debian/changelog b/debian/changelog
index 06fb028..3dbd078 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,3 +1,9 @@
+why (2.34-3) UNRELEASED; urgency=medium
+
+ * improve as-installed package tests
+
+ -- Ralf Treinen <trei...@debian.org> Thu, 16 Oct 2014 22:08:01 +0200
+
why (2.34-2) unstable; urgency=medium
* Team upload
diff --git a/debian/tests/control b/debian/tests/control
index 1a3e116..7205044 100644
--- a/debian/tests/control
+++ b/debian/tests/control
@@ -1,15 +1,11 @@
Tests: why+alt-ergo
-Depends: @, alt-ergo
-Restrictions: allow-stderr
+Depends: why, alt-ergo
Tests: why+cvc3
-Depends: @, cvc3
-Restrictions: allow-stderr
+Depends: why, cvc3
Tests: why+coq
-Depends: @, coq
-Restrictions: allow-stderr
+Depends: why, libwhy-coq, coq
Tests: frama-c+jessie+alt-ergo
-Depends: @, frama-c-base, alt-ergo
-Restrictions: allow-stderr
+Depends: why, frama-c-base, alt-ergo
diff --git a/debian/tests/frama-c+jessie+alt-ergo
b/debian/tests/frama-c+jessie+alt-ergo
index 92722e0..b133444 100755
--- a/debian/tests/frama-c+jessie+alt-ergo
+++ b/debian/tests/frama-c+jessie+alt-ergo
@@ -2,25 +2,26 @@
set -e
+this=frama-c+jessie+alt-ergo
indir=${PWD}/debian/tests/c
-outdir=${TMPDIR-/tmp}
+outdir=${ADT_ARTIFACTS}/${this}
+mkdir -p ${outdir}
-if [ ! -f ${HOME}/.whyrc ]; then why-config > /dev/null 2>&1; fi
+# why expects a ${HOME}/.whyrc :-(
+export HOME=${ADTTMP}
+why-config > /dev/null 2>&1
cd ${outdir}
for infile in ${indir}/minimum.c
do
base=$(basename $infile)
- # we copy the input file into the tmpdir since jessie insists on
+ # we copy the input file into the outdir since jessie insists on
# creating "project" files in the directory of the input file :-(
cp ${infile} .
framacoutfile=${base%.c}.frc
- echo "Testing frama-c + jessie + alt-ergo on $base" >&2
successpattern="why/${base%.c}_why.why : .. (2/0/0/0/0)"
- frama-c -jessie -jessie-atp=alt-ergo ${base} > ${framacoutfile}
- if ! $(grep -q "${successpattern}" ${framacoutfile}); then
- cat ${framacoutfile}
- exit 1
- fi
+ frama-c -jessie -jessie-atp=alt-ergo ${base} \
+ | tee ${framacoutfile} \
+ | grep -q "${successpattern}"
done
diff --git a/debian/tests/why+alt-ergo b/debian/tests/why+alt-ergo
index fb99ab9..7acf8d8 100755
--- a/debian/tests/why+alt-ergo
+++ b/debian/tests/why+alt-ergo
@@ -2,20 +2,17 @@
set -e
+this=why+alt-ergo
indir=debian/tests/why
-outdir=${TMPDIR-/tmp}
+outdir=${ADT_ARTIFACTS}/${this}
+mkdir -p ${outdir}
# alt-ergo cannot prove the VC of racine :-(
for infile in $indir/minimum.why $indir/gauss.why
do
base=$(basename $infile)
- echo "Testing why + alt-ergo on $base" >&2
whyoutfile=$outdir/${base%.why}_why.why
altoutfile=$outdir/${base%.why}.ae
why --alt-ergo --output $whyoutfile $infile
- alt-ergo $whyoutfile > $altoutfile
- if $(grep -qv "Valid" $altoutfile); then
- cat $altoutfile
- exit 1
- fi
-done
\ No newline at end of file
+ alt-ergo $whyoutfile | tee $altoutfile | grep -q "Valid"
+done
diff --git a/debian/tests/why+coq b/debian/tests/why+coq
index 7cdbffd..883c8a7 100755
--- a/debian/tests/why+coq
+++ b/debian/tests/why+coq
@@ -2,17 +2,18 @@
set -e
+this=why+coq
indir=debian/tests/why
-outdir=${TMPDIR-/tmp}
+outdir=${ADT_ARTIFACTS}/${this}
+mkdir -p ${outdir}
for infile in $indir/minimum.why
do
base=$(basename $infile)
- echo "Testing why + coq on $base" >&2
whyoutfile=$outdir/${base%.why}
coqinfile=${whyoutfile}_proof.v
why --coq --no-coq-use-dp --output $whyoutfile $infile
sed -e 's/(\* FILL PROOF HERE \*)/intros; subst; auto using min_ax./' \
< ${whyoutfile}_why.v > ${coqinfile}
coqc ${coqinfile}
-done
\ No newline at end of file
+done
diff --git a/debian/tests/why+cvc3 b/debian/tests/why+cvc3
index 6df7332..2badcf7 100755
--- a/debian/tests/why+cvc3
+++ b/debian/tests/why+cvc3
@@ -2,19 +2,16 @@
set -e
+this=why+cvc3
indir=debian/tests/why
-outdir=${TMPDIR-/tmp}
+outdir=${ADT_ARTIFACTS}/${this}
+mkdir -p ${outdir}
for infile in $indir/*.why
do
base=$(basename $infile)
- echo "Testing why + cvc3 on $base" >&2
whyoutfile=$outdir/${base%.why}_why.cvc
cvcoutfile=$outdir/${base%.why}.cvcout
why --cvcl --output $whyoutfile $infile
- cvc3 $whyoutfile > $cvcoutfile
- if $(grep -qv "Valid" $cvcoutfile); then
- cat $cvcoutfile
- exit 1
- fi
-done
\ No newline at end of file
+ cvc3 $whyoutfile | tee $cvcoutfile | grep -q "Valid"
+done
--
Alioth's /usr/local/bin/git-commit-notice on
/srv/git.debian.org/git/pkg-ocaml-maint/packages/why.git
_______________________________________________
Pkg-ocaml-maint-commits mailing list
Pkg-ocaml-maint-commits@lists.alioth.debian.org
http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits
