[Pkg-ocaml-maint-commits] [why] 01/01: add krakatoa test

[Ralf Treinen]

This is an automated email from the git hooks/post-receive script.

treinen pushed a commit to branch master
in repository why.

commit f03921b2ef4047bab69ad3b315acb89cc486f0f6
Author: Ralf Treinen <treinen at free.fr>
Date:   Wed Oct 5 08:19:04 2016 +0200

    add krakatoa test
---
 debian/changelog               |  3 ++-
 debian/tests/control           |  5 ++++-
 debian/tests/java/Minimum.java |  9 +++++++++
 debian/tests/krakatoa+alt-ergo | 21 +++++++++++++++++++++
 4 files changed, 36 insertions(+), 2 deletions(-)

diff --git a/debian/changelog b/debian/changelog
index 83d78b2..ca10733 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -32,9 +32,10 @@ why (2.36-1) UNRELEASED; urgency=medium
   * drop autoconf from d/rules and from build-dependencies
   * d/rules: disable upstream tests
   * d/rules: create bin directory before invoking dh_auto_build
+  * d/tests: add test krakato+alt-ergo
   * remove d/README.source which is obsolete.
 
- -- Ralf Treinen <treinen at debian.org>  Tue, 04 Oct 2016 21:14:23 +0200
+ -- Ralf Treinen <treinen at debian.org>  Wed, 05 Oct 2016 08:27:12 +0200
 
 why (2.34-4) unstable; urgency=medium
 
diff --git a/debian/tests/control b/debian/tests/control
index 38c11fd..47b5e50 100644
--- a/debian/tests/control
+++ b/debian/tests/control
@@ -1,2 +1,5 @@
 Tests: frama-c+jessie+alt-ergo
-Depends: why, frama-c-base, alt-ergo
+Depends: why, alt-ergo
+
+Tests: krakatoa+alt-ergo
+Depends: why, alt-ergo
diff --git a/debian/tests/java/Minimum.java b/debian/tests/java/Minimum.java
new file mode 100644
index 0000000..e13fabe
--- /dev/null
+++ b/debian/tests/java/Minimum.java
@@ -0,0 +1,9 @@
+public class Minimum {
+
+    /*@ ensures (\result >= i && \result >= j);  
+      @*/
+    
+    public static int max(int i, int j) { 
+	if (i < j) return j; else return i; 
+    }
+}
diff --git a/debian/tests/krakatoa+alt-ergo b/debian/tests/krakatoa+alt-ergo
new file mode 100755
index 0000000..b1e6a83
--- /dev/null
+++ b/debian/tests/krakatoa+alt-ergo
@@ -0,0 +1,21 @@
+#!/bin/sh
+
+set -e
+
+this=krakatoa+alt-ergo
+indir=${PWD}/debian/tests/java
+outdir=${ADT_ARTIFACTS}/${this}
+mkdir -p ${outdir}
+
+why3 config --detect-provers > /dev/null 2>&1
+
+cd ${outdir}
+
+for infile in ${indir}/Minimum.java
+do
+    base=$(basename $infile)
+    # we copy the input file into the outdir since jessie insists on
+    # creating "project" files in the directory of the input file :-(
+    cp ${infile} .
+    krakatoa -why3 "prove -P alt-ergo" ${base} 2>&1 | grep -q "Valid"
+done

-- 
Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/why.git