[Pkg-ocaml-maint-commits] [why] 20/21: adapt jessie test to why3

Ralf Treinen treinen at moszumanska.debian.org
Tue Oct 4 19:16:36 UTC 2016


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

treinen pushed a commit to branch master
in repository why.

commit 5eabf0fea7cf52997b96762b4171881c8213ecc4
Author: Ralf Treinen <treinen at free.fr>
Date:   Tue Oct 4 20:44:16 2016 +0200

    adapt jessie test to why3
---
 debian/changelog                     |  1 +
 debian/tests/frama-c+jessie+alt-ergo | 11 +++--------
 2 files changed, 4 insertions(+), 8 deletions(-)

diff --git a/debian/changelog b/debian/changelog
index 22a7a37..e098091 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -12,6 +12,7 @@ why (2.36-1) UNRELEASED; urgency=medium
     - remove d/why.links as upstream does not ship the why manpage any more
     - add build-dependency on why3
     - package why: add dependency on why3
+    - d/tests/frama-c+jessie+alt-ergo: adapt to why3
     - package why: remove Recommends of SMT solvers
     - remove tests why+{alt-ergo,coq,cvc3}
   * Due to disappearance of doc/manual.ps and ocamlgraph/ from upstream:
diff --git a/debian/tests/frama-c+jessie+alt-ergo b/debian/tests/frama-c+jessie+alt-ergo
index b133444..d16974d 100755
--- a/debian/tests/frama-c+jessie+alt-ergo
+++ b/debian/tests/frama-c+jessie+alt-ergo
@@ -7,9 +7,7 @@ indir=${PWD}/debian/tests/c
 outdir=${ADT_ARTIFACTS}/${this}
 mkdir -p ${outdir}
 
-# why expects a ${HOME}/.whyrc :-(
-export HOME=${ADTTMP}
-why-config  > /dev/null 2>&1
+why3 config --detect-provers > /dev/null 2>&1
 
 cd ${outdir}
 
@@ -19,9 +17,6 @@ do
     # 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
-    successpattern="why/${base%.c}_why.why           : .. (2/0/0/0/0)"
-    frama-c -jessie -jessie-atp=alt-ergo ${base} \
-        | tee ${framacoutfile} \
-	| grep -q "${successpattern}"
+    frama-c -jessie -jessie-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



More information about the Pkg-ocaml-maint-commits mailing list