This is an automated email from the git hooks/post-receive script.
treinen pushed a commit to branch master
in repository why.
commit b50d5aa0a0f77abce9798be7d801634719de392b
Author: Ralf Treinen <trei...@free.fr>
Date: Sun Jan 19 20:08:10 2014 +0100
package tests with alt-ergo, cvc3
---
debian/changelog | 3 ++-
debian/control | 1 +
debian/tests/control | 7 +++++++
debian/tests/why+alt-ergo | 21 +++++++++++++++++++++
debian/tests/why+cvc3 | 20 ++++++++++++++++++++
debian/tests/why/gauss.why | 18 ++++++++++++++++++
debian/tests/why/minimum.why | 4 ++++
debian/tests/why/racine.why | 20 ++++++++++++++++++++
8 files changed, 93 insertions(+), 1 deletion(-)
diff --git a/debian/changelog b/debian/changelog
index ad2c0a2..d6e0b46 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -17,8 +17,9 @@ why (2.33-1) unstable; urgency=low
alt-ergo, coq
* Add myself to uploaders.
* Standards-Version 3.9.5 (no change)
+ * Add DEP8-style package tests for why with alt-ergo, and why with cvc3.
- -- Ralf Treinen <trei...@debian.org> Fri, 17 Jan 2014 20:36:07 +0100
+ -- Ralf Treinen <trei...@debian.org> Sun, 19 Jan 2014 20:07:21 +0100
why (2.30+dfsg-5) unstable; urgency=low
diff --git a/debian/control b/debian/control
index 125751d..b95eba3 100644
--- a/debian/control
+++ b/debian/control
@@ -24,6 +24,7 @@ Standards-Version: 3.9.5
Homepage: http://why.lri.fr/
Vcs-Browser: http://git.debian.org/?p=pkg-ocaml-maint/packages/why.git
Vcs-Git: git://git.debian.org/git/pkg-ocaml-maint/packages/why.git
+XS-Testsuite: autopkgtest
Package: why
Architecture: any
diff --git a/debian/tests/control b/debian/tests/control
new file mode 100644
index 0000000..f09e8f9
--- /dev/null
+++ b/debian/tests/control
@@ -0,0 +1,7 @@
+Tests: why+alt-ergo
+Depends: @, alt-ergo
+Restrictions: allow-stderr
+
+Tests: why+cvc3
+Depends: @, cvc3
+Restrictions: allow-stderr
diff --git a/debian/tests/why+alt-ergo b/debian/tests/why+alt-ergo
new file mode 100755
index 0000000..fb99ab9
--- /dev/null
+++ b/debian/tests/why+alt-ergo
@@ -0,0 +1,21 @@
+#!/bin/sh
+
+set -e
+
+indir=debian/tests/why
+outdir=${TMPDIR-/tmp}
+
+# 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
diff --git a/debian/tests/why+cvc3 b/debian/tests/why+cvc3
new file mode 100755
index 0000000..6df7332
--- /dev/null
+++ b/debian/tests/why+cvc3
@@ -0,0 +1,20 @@
+#!/bin/sh
+
+set -e
+
+indir=debian/tests/why
+outdir=${TMPDIR-/tmp}
+
+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
diff --git a/debian/tests/why/gauss.why b/debian/tests/why/gauss.why
new file mode 100644
index 0000000..d6c1517
--- /dev/null
+++ b/debian/tests/why/gauss.why
@@ -0,0 +1,18 @@
+let gauss (y: int) =
+
+{y > 0}
+ let x = ref 0 in
+ let z = ref 0 in
+
+ while ( !z < y) do
+
+ {invariant z <= y and 2*x = z*(z+1)}
+
+ z := !z + 1;
+ x := !x + !z
+
+ done;
+
+ !x
+
+{2*result = y*(y+1)}
diff --git a/debian/tests/why/minimum.why b/debian/tests/why/minimum.why
new file mode 100644
index 0000000..602e478
--- /dev/null
+++ b/debian/tests/why/minimum.why
@@ -0,0 +1,4 @@
+logic min: int, int -> int
+axiom min_ax: forall x,y:int. min(x,y) <= x
+parameter r: int ref
+let f (n:int) = r := min !r n { r <= r@ }
diff --git a/debian/tests/why/racine.why b/debian/tests/why/racine.why
new file mode 100644
index 0000000..1d5f525
--- /dev/null
+++ b/debian/tests/why/racine.why
@@ -0,0 +1,20 @@
+let racine (x: int) =
+{x >= 0}
+
+ let y1 = ref 0 in
+ let y2 = ref 1 in
+ let y3 = ref 1 in
+
+ while ( !y3 <= x) do
+
+ {invariant y2 = 2*y1+1 and y3 = (y1+1)*(y1+1) and y1*y1 <= x}
+
+ y1 := !y1 + 1;
+ y2 := !y2 + 2;
+ y3 := !y3 + !y2
+
+ done;
+
+ !y1
+
+{result*result<=x and (result+1)*(result+1)>x}
--
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
