[Pkg-ocaml-maint-commits] [why] 01/01: add test of jessie plugin

[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 75888ee420ca5cd8d8c5fa0d9e03d08c2ffd329c
Author: Ralf Treinen <treinen at pps.univ-paris-diderot.fr>
Date:   Thu Feb 13 18:25:41 2014 +0100

    add test of jessie plugin
---
 debian/changelog                     |  1 +
 debian/tests/c/minimum.c             |  4 ++++
 debian/tests/control                 |  4 ++++
 debian/tests/frama-c+jessie+alt-ergo | 28 ++++++++++++++++++++++++++++
 4 files changed, 37 insertions(+)

diff --git a/debian/changelog b/debian/changelog
index 4a7a46d..ddb0c23 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -22,6 +22,7 @@ why (2.33-1) unstable; urgency=low
     - why with alt-ergo
     - why with cvc3
     - why with coq (thanks to Pierre Letouzey for his help!)
+    - frama-c, jessie plugin (from the why package), and alt-ergo
   * Add to the Recommendation of package alt-ergo alternatives on other
     theorem provers: cvc3, coq
   * Bump build-dependency on frama-c-base to the latest version.
diff --git a/debian/tests/c/minimum.c b/debian/tests/c/minimum.c
new file mode 100644
index 0000000..1d356eb
--- /dev/null
+++ b/debian/tests/c/minimum.c
@@ -0,0 +1,4 @@
+//@ ensures \result == \max(i,j); 
+int max(int i, int j) { 
+  return (i < j) ? j : i; 
+} 
diff --git a/debian/tests/control b/debian/tests/control
index 88f892c..426cb75 100644
--- a/debian/tests/control
+++ b/debian/tests/control
@@ -9,3 +9,7 @@ Restrictions: allow-stderr
 Tests: why+coq
 Depends: @, coq
 Restrictions: allow-stderr
+
+Tests: frama-c+jessie+alt-ergo
+Depends: @, frama-c-base, cpp-4.7. alt-ergo
+Restrictions: allow-stderr
diff --git a/debian/tests/frama-c+jessie+alt-ergo b/debian/tests/frama-c+jessie+alt-ergo
new file mode 100755
index 0000000..392c607
--- /dev/null
+++ b/debian/tests/frama-c+jessie+alt-ergo
@@ -0,0 +1,28 @@
+#!/bin/sh
+
+set -e
+
+indir=${PWD}/debian/tests/c
+outdir=${TMPDIR-/tmp}
+
+cd ${outdir}
+
+for infile in ${indir}/minimum.c
+do
+    base=$(basename $infile)
+    # we copy the input file into the tmpdir 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 \
+	-cpp-command 'cpp-4.7 -C -E -I.' ${base} > ${framacoutfile}
+    if ! $(grep -q "${successpattern}" ${framacoutfile}); then
+    	cat ${framacoutfile}
+    	exit 1
+    fi
+done
+
+# we have to use cpp-4.7, see
+# http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2013-November/004057.html
\ No newline at end of file

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