[cvc4] 10/10: Add hello-world test in debian/tests/

Fabian Wolff fw-guest at moszumanska.debian.org
Tue Jul 11 23:02:05 UTC 2017


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

fw-guest pushed a commit to branch master
in repository cvc4.

commit 80a6dadcdea43e1c7cad47a56761b83d2214726d
Author: Fabian Wolff <fabi.wolff at arcor.de>
Date:   Wed Jul 12 00:41:27 2017 +0200

    Add hello-world test in debian/tests/
---
 debian/control           |  3 ++-
 debian/tests/control     |  2 ++
 debian/tests/hello-world | 31 +++++++++++++++++++++++++++++++
 3 files changed, 35 insertions(+), 1 deletion(-)

diff --git a/debian/control b/debian/control
index e5ecc64..ae8117e 100644
--- a/debian/control
+++ b/debian/control
@@ -44,7 +44,8 @@ Section: libdevel
 Depends: libcvc4-4 (= ${binary:Version}),
          libcvc4parser4 (= ${binary:Version}),
          ${shlibs:Depends},
-         ${misc:Depends}
+         ${misc:Depends},
+         libgmp-dev
 Description: automated theorem prover for SMT problems (development files)
  CVC4 is an efficient automatic theorem prover for satisfiability
  modulo theories (SMT) problems. It can be used to prove the validity
diff --git a/debian/tests/control b/debian/tests/control
new file mode 100644
index 0000000..e496246
--- /dev/null
+++ b/debian/tests/control
@@ -0,0 +1,2 @@
+Tests: hello-world
+Depends: @, build-essential
diff --git a/debian/tests/hello-world b/debian/tests/hello-world
new file mode 100755
index 0000000..6339b46
--- /dev/null
+++ b/debian/tests/hello-world
@@ -0,0 +1,31 @@
+#!/bin/sh
+
+set -e
+
+TMPDIR=$(mktemp -d)
+trap "rm -rf $TMPDIR" EXIT
+cd $TMPDIR
+
+cat <<EOF > hello-world.cc
+#include <iostream>
+#include <cvc4/cvc4.h>
+
+using namespace CVC4;
+
+int main ()
+{
+    ExprManager em;
+    Expr helloWorld = em.mkVar ("Hello world!", em.booleanType ());
+    SmtEngine smt (&em);
+
+    std::cout << helloWorld << " is " << smt.query (helloWorld) << std::endl;
+    return 0;
+}
+EOF
+
+c++ -o hello-world hello-world.cc -lcvc4 -Wno-deprecated
+[ -x hello-world ]
+
+./hello-world > output
+echo "Hello world! is invalid" > expected
+diff expected output

-- 
Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/debian-science/packages/cvc4.git



More information about the debian-science-commits mailing list