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 <trei...@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 _______________________________________________ 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