From c3a6ff8c6e4a0c743cd33eb29931f837eeb2959e Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 8 Apr 2010 20:49:11 +0000 Subject: A handful of build system fixes: * (test/unit/Makefile.am) libtool was being passed relative paths of sources in .cpp, confusing lcov if -b wasn't given. Fixed. Closes bug #102. * (configure.ac) --enable-coverage now implies --enable-static --enable-static-binary --disable-shared. * (configure.ac) Create top-level config.status for informational and re-configuration purposes. * (configure.ac) Remove -fvisibility=hidden for debug builds. Closes bug #104. * (test/unit/Makefile.am) Build unit tests with -Wall. * (various unit tests) Fixed trivially-fixable warnings in building unit tests. (Signedness in comparison, unused variables, etc.) * (Makefile.builds.in) Copy the binary correctly if it is static. (It was failing, but only with --enable-static --enable-shared --enable-static-binary.) Closes bug #103. * (src/parser/Makefile.am) libcvc4parser.so now links with libcvc4.so. * Other minor cleanups to the build system. --- test/unit/expr/attribute_white.h | 4 --- test/unit/expr/node_black.h | 6 ++-- test/unit/expr/node_builder_black.h | 68 ++++++++++++++++++------------------- test/unit/expr/node_manager_black.h | 30 ++++++++-------- test/unit/expr/node_white.h | 2 +- 5 files changed, 53 insertions(+), 57 deletions(-) (limited to 'test/unit/expr') diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h index e0d9d6bf4..e3b7811a4 100644 --- a/test/unit/expr/attribute_white.h +++ b/test/unit/expr/attribute_white.h @@ -149,8 +149,6 @@ public: } void testCDAttributes() { - AttributeManager& am = d_nm->d_attrManager; - //Debug.on("boolattr"); Node a = d_nm->mkVar(d_booleanType); @@ -279,8 +277,6 @@ public: } void testAttributes() { - AttributeManager& am = d_nm->d_attrManager; - //Debug.on("boolattr"); Node a = d_nm->mkVar(d_booleanType); diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 17657683d..23d1daf4e 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -423,10 +423,10 @@ public: #endif /* CVC4_ASSERTIONS */ } - void testNaryExpForSize(Kind k, int N) { + void testNaryExpForSize(Kind k, unsigned N) { NodeBuilder<> nbz(k); Node trueNode = d_nodeManager->mkConst(true); - for(int i = 0; i < N; ++i) { + for(unsigned i = 0; i < N; ++i) { nbz << trueNode; } Node result = nbz; @@ -452,7 +452,7 @@ public: srand(0); int trials = 500; for(int i = 0; i < trials; ++i) { - int N = rand() % 1000 + 2; + unsigned N = rand() % 1000 + 2; testNaryExpForSize(AND, N); } diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index eec6949f0..4521f3bf6 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -64,8 +64,8 @@ public: } } -#define K 30 -#define LARGE_K UINT_MAX/40 +#define K 30u +#define LARGE_K UINT_MAX / 40 Kind specKind; @@ -84,23 +84,23 @@ public: /* default size tests */ NodeBuilder<> def; TS_ASSERT_EQUALS(def.getKind(), UNDEFINED_KIND); - TS_ASSERT_EQUALS(def.getNumChildren(), 0); + TS_ASSERT_EQUALS(def.getNumChildren(), 0u); TS_ASSERT_EQUALS(def.begin(), def.end()); NodeBuilder<> spec(specKind); TS_ASSERT_EQUALS(spec.getKind(), specKind); - TS_ASSERT_EQUALS(spec.getNumChildren(), 0); + TS_ASSERT_EQUALS(spec.getNumChildren(), 0u); TS_ASSERT_EQUALS(spec.begin(), spec.end()); NodeBuilder<> from_nm(d_nm); TS_ASSERT_EQUALS(from_nm.getKind(), UNDEFINED_KIND); - TS_ASSERT_EQUALS(from_nm.getNumChildren(), 0); + TS_ASSERT_EQUALS(from_nm.getNumChildren(), 0u); TS_ASSERT_EQUALS(from_nm.begin(), from_nm.end()); NodeBuilder<> from_nm_kind(d_nm, specKind); TS_ASSERT_EQUALS(from_nm_kind.getKind(), specKind); - TS_ASSERT_EQUALS(from_nm_kind.getNumChildren(), 0); + TS_ASSERT_EQUALS(from_nm_kind.getNumChildren(), 0u); TS_ASSERT_EQUALS(from_nm_kind.begin(), from_nm_kind.end()); @@ -108,23 +108,23 @@ public: NodeBuilder ws; TS_ASSERT_EQUALS(ws.getKind(), UNDEFINED_KIND); - TS_ASSERT_EQUALS(ws.getNumChildren(), 0); + TS_ASSERT_EQUALS(ws.getNumChildren(), 0u); TS_ASSERT_EQUALS(ws.begin(), ws.end()); NodeBuilder ws_kind(specKind); TS_ASSERT_EQUALS(ws_kind.getKind(), specKind); - TS_ASSERT_EQUALS(ws_kind.getNumChildren(), 0); + TS_ASSERT_EQUALS(ws_kind.getNumChildren(), 0u); TS_ASSERT_EQUALS(ws_kind.begin(), ws_kind.end()); NodeBuilder ws_from_nm(d_nm); TS_ASSERT_EQUALS(ws_from_nm.getKind(), UNDEFINED_KIND); - TS_ASSERT_EQUALS(ws_from_nm.getNumChildren(), 0); + TS_ASSERT_EQUALS(ws_from_nm.getNumChildren(), 0u); TS_ASSERT_EQUALS(ws_from_nm.begin(), ws_from_nm.end()); NodeBuilder ws_from_nm_kind(d_nm, specKind); TS_ASSERT_EQUALS(ws_from_nm_kind.getKind(), specKind); - TS_ASSERT_EQUALS(ws_from_nm_kind.getNumChildren(), 0); + TS_ASSERT_EQUALS(ws_from_nm_kind.getNumChildren(), 0u); TS_ASSERT_EQUALS(ws_from_nm_kind.begin(), ws_from_nm_kind.end()); @@ -137,23 +137,23 @@ public: NodeBuilder<> copy(def); TS_ASSERT_EQUALS(copy.getKind(), UNDEFINED_KIND); - TS_ASSERT_EQUALS(copy.getNumChildren(), 0); + TS_ASSERT_EQUALS(copy.getNumChildren(), 0u); TS_ASSERT_EQUALS(copy.begin(), copy.end()); NodeBuilder cp_ws(ws); TS_ASSERT_EQUALS(cp_ws.getKind(), UNDEFINED_KIND); - TS_ASSERT_EQUALS(cp_ws.getNumChildren(), 0); + TS_ASSERT_EQUALS(cp_ws.getNumChildren(), 0u); TS_ASSERT_EQUALS(cp_ws.begin(), cp_ws.end()); NodeBuilder cp_from_larger(ws); TS_ASSERT_EQUALS(cp_from_larger.getKind(), UNDEFINED_KIND); - TS_ASSERT_EQUALS(cp_from_larger.getNumChildren(), 0); + TS_ASSERT_EQUALS(cp_from_larger.getNumChildren(), 0u); TS_ASSERT_EQUALS(cp_from_larger.begin(), cp_from_larger.end()); NodeBuilder cp_from_smaller(ws); TS_ASSERT_EQUALS(cp_from_smaller.getKind(), UNDEFINED_KIND); - TS_ASSERT_EQUALS(cp_from_smaller.getNumChildren(), 0); + TS_ASSERT_EQUALS(cp_from_smaller.getNumChildren(), 0u); TS_ASSERT_EQUALS(cp_from_smaller.begin(), cp_from_smaller.end()); } @@ -174,14 +174,14 @@ public: TS_ASSERT_DIFFERS(ws.begin(), ws.end()); NodeBuilder::iterator iter = ws.begin(); - for(int i = 0; i < K; ++i){ + for(unsigned i = 0; i < K; ++i){ TS_ASSERT_DIFFERS(iter, ws.end()); ++iter; } TS_ASSERT_EQUALS(iter, ws.end()); NodeBuilder::const_iterator citer = ws.begin(); - for(int i = 0; i < K; ++i){ + for(unsigned i = 0; i < K; ++i){ TS_ASSERT_DIFFERS(citer, ws.end()); ++citer; } @@ -196,14 +196,14 @@ public: TS_ASSERT_DIFFERS(smaller.begin(), smaller.end()); NodeBuilder<>::iterator smaller_iter = smaller.begin(); - for(int i = 0; i < K; ++i){ + for(unsigned i = 0; i < K; ++i){ TS_ASSERT_DIFFERS(smaller_iter, smaller.end()); ++smaller_iter; } TS_ASSERT_EQUALS(iter, ws.end()); NodeBuilder<>::const_iterator smaller_citer = smaller.begin(); - for(int i = 0; i < K; ++i){ + for(unsigned i = 0; i < K; ++i){ TS_ASSERT_DIFFERS(smaller_citer, smaller.end()); ++smaller_citer; } @@ -261,24 +261,24 @@ public: /* unsigned getNumChildren() const; */ NodeBuilder<> noKind; - TS_ASSERT_EQUALS(noKind.getNumChildren(), 0); + TS_ASSERT_EQUALS(noKind.getNumChildren(), 0u); push_back(noKind, K); TS_ASSERT_EQUALS(noKind.getNumChildren(), K); push_back(noKind, K); - TS_ASSERT_EQUALS(noKind.getNumChildren(), K+K); + TS_ASSERT_EQUALS(noKind.getNumChildren(), K + K); noKind << AND;// avoid exception on marking it used Node n = noKind;// avoid warning on clear() noKind.clear(); - TS_ASSERT_EQUALS(noKind.getNumChildren(), 0); + TS_ASSERT_EQUALS(noKind.getNumChildren(), 0u); push_back(noKind, K); TS_ASSERT_EQUALS(noKind.getNumChildren(), K); push_back(noKind, K); - TS_ASSERT_EQUALS(noKind.getNumChildren(), K+K); + TS_ASSERT_EQUALS(noKind.getNumChildren(), K + K); #ifdef CVC4_ASSERTIONS noKind << specKind; @@ -320,7 +320,7 @@ public: TS_ASSERT_EQUALS(arr[0], i_0); TS_ASSERT_EQUALS(arr[2], i_2); - for(int i = 3; i < K; ++i) { + for(unsigned i = 3; i < K; ++i) { TS_ASSERT_EQUALS(arr[i], d_nm->mkConst(true)); } @@ -328,7 +328,7 @@ public: TS_ASSERT_EQUALS(arr[0], i_0); TS_ASSERT_EQUALS(arr[2], i_2); - for(int i = 3; i < K; ++i) { + for(unsigned i = 3; i < K; ++i) { TS_ASSERT_EQUALS(arr[i], d_nm->mkConst(true)); } TS_ASSERT_EQUALS(arr[K], i_K); @@ -344,7 +344,7 @@ public: NodeBuilder<> nb; TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND); - TS_ASSERT_EQUALS(nb.getNumChildren(), 0); + TS_ASSERT_EQUALS(nb.getNumChildren(), 0u); TS_ASSERT_EQUALS(nb.begin(), nb.end()); nb << specKind; @@ -358,7 +358,7 @@ public: nb.clear(); TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND); - TS_ASSERT_EQUALS(nb.getNumChildren(), 0); + TS_ASSERT_EQUALS(nb.getNumChildren(), 0u); TS_ASSERT_EQUALS(nb.begin(), nb.end()); nb << specKind; @@ -372,7 +372,7 @@ public: nb.clear(specKind); TS_ASSERT_EQUALS(nb.getKind(), specKind); - TS_ASSERT_EQUALS(nb.getNumChildren(), 0); + TS_ASSERT_EQUALS(nb.getNumChildren(), 0u); TS_ASSERT_EQUALS(nb.begin(), nb.end()); push_back(nb, K); @@ -380,7 +380,7 @@ public: nb.clear(); TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND); - TS_ASSERT_EQUALS(nb.getNumChildren(), 0); + TS_ASSERT_EQUALS(nb.getNumChildren(), 0u); TS_ASSERT_EQUALS(nb.begin(), nb.end()); } @@ -437,7 +437,7 @@ public: /* NodeBuilder& operator<<(const Node& n); */ NodeBuilder nb(specKind); TS_ASSERT_EQUALS(nb.getKind(), specKind); - TS_ASSERT_EQUALS(nb.getNumChildren(), 0); + TS_ASSERT_EQUALS(nb.getNumChildren(), 0u); TS_ASSERT_EQUALS(nb.begin(), nb.end()); push_back(nb,K); TS_ASSERT_EQUALS(nb.getKind(), specKind); @@ -451,13 +451,13 @@ public: NodeBuilder<> overflow(specKind); TS_ASSERT_EQUALS(overflow.getKind(), specKind); - TS_ASSERT_EQUALS(overflow.getNumChildren(), 0); + TS_ASSERT_EQUALS(overflow.getNumChildren(), 0u); TS_ASSERT_EQUALS(overflow.begin(), overflow.end()); push_back(overflow,5*K+1); TS_ASSERT_EQUALS(overflow.getKind(), specKind); - TS_ASSERT_EQUALS(overflow.getNumChildren(), 5*K+1); + TS_ASSERT_EQUALS(overflow.getNumChildren(), 5 * K + 1); TS_ASSERT_DIFFERS(overflow.begin(), overflow.end()); } @@ -598,16 +598,16 @@ public: Node f = d_nm->mkVar(d_booleanType); Node m = a && b; - Node n = a && b || c; + Node n = (a && b) || c; Node o = d + e - b; - Node p = a && o || c; + Node p = (a && o) || c; Node x = d + e + o - m; Node y = f - a - c + e; Node q = a && b && c; - Node r = e && d && b && a || x && y || f || q && a; + Node r = (e && d && b && a) || (x && y) || f || (q && a); TS_ASSERT_EQUALS(m, d_nm->mkNode(AND, a, b)); TS_ASSERT_EQUALS(n, d_nm->mkNode(OR, m, c)); diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h index 3e65be0b7..e059fa509 100644 --- a/test/unit/expr/node_manager_black.h +++ b/test/unit/expr/node_manager_black.h @@ -52,7 +52,7 @@ public: void testMkNode1() { Node x = d_nodeManager->mkVar("x",d_nodeManager->booleanType()); Node n = d_nodeManager->mkNode(NOT, x); - TS_ASSERT_EQUALS( n.getNumChildren(), 1 ); + TS_ASSERT_EQUALS( n.getNumChildren(), 1u ); TS_ASSERT_EQUALS( n.getKind(), NOT); TS_ASSERT_EQUALS( n[0], x); } @@ -61,7 +61,7 @@ public: Node x = d_nodeManager->mkVar("x",d_nodeManager->booleanType()); Node y = d_nodeManager->mkVar("y",d_nodeManager->booleanType()); Node n = d_nodeManager->mkNode(IMPLIES, x, y); - TS_ASSERT_EQUALS( n.getNumChildren(), 2 ); + TS_ASSERT_EQUALS( n.getNumChildren(), 2u ); TS_ASSERT_EQUALS( n.getKind(), IMPLIES); TS_ASSERT_EQUALS( n[0], x); TS_ASSERT_EQUALS( n[1], y); @@ -72,7 +72,7 @@ public: Node y = d_nodeManager->mkVar("y",d_nodeManager->booleanType()); Node z = d_nodeManager->mkVar("z",d_nodeManager->booleanType()); Node n = d_nodeManager->mkNode(AND, x, y, z); - TS_ASSERT_EQUALS( n.getNumChildren(), 3 ); + TS_ASSERT_EQUALS( n.getNumChildren(), 3u ); TS_ASSERT_EQUALS( n.getKind(), AND); TS_ASSERT_EQUALS( n[0], x); TS_ASSERT_EQUALS( n[1], y); @@ -85,12 +85,12 @@ public: Node x3 = d_nodeManager->mkVar("x3",d_nodeManager->booleanType()); Node x4 = d_nodeManager->mkVar("x4",d_nodeManager->booleanType()); Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4); - TS_ASSERT_EQUALS( n.getNumChildren(), 4 ); - TS_ASSERT_EQUALS( n.getKind(), AND); - TS_ASSERT_EQUALS( n[0], x1); - TS_ASSERT_EQUALS( n[1], x2); - TS_ASSERT_EQUALS( n[2], x3); - TS_ASSERT_EQUALS( n[3], x4); + TS_ASSERT_EQUALS( n.getNumChildren(), 4u ); + TS_ASSERT_EQUALS( n.getKind(), AND ); + TS_ASSERT_EQUALS( n[0], x1 ); + TS_ASSERT_EQUALS( n[1], x2 ); + TS_ASSERT_EQUALS( n[2], x3 ); + TS_ASSERT_EQUALS( n[3], x4 ); } void testMkNode5() { @@ -100,7 +100,7 @@ public: Node x4 = d_nodeManager->mkVar("x4",d_nodeManager->booleanType()); Node x5 = d_nodeManager->mkVar("x5",d_nodeManager->booleanType()); Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4, x5); - TS_ASSERT_EQUALS( n.getNumChildren(), 5 ); + TS_ASSERT_EQUALS( n.getNumChildren(), 5u ); TS_ASSERT_EQUALS( n.getKind(), AND); TS_ASSERT_EQUALS( n[0], x1); TS_ASSERT_EQUALS( n[1], x2); @@ -120,7 +120,7 @@ public: Node n = d_nodeManager->mkNode(AND, args); TS_ASSERT_EQUALS( n.getNumChildren(), args.size() ); TS_ASSERT_EQUALS( n.getKind(), AND); - for( int i=0; i < args.size(); ++i ) { + for( unsigned i = 0; i < args.size(); ++i ) { TS_ASSERT_EQUALS( n[i], args[i]); } } @@ -136,7 +136,7 @@ public: Node n = d_nodeManager->mkNode(AND, args); TS_ASSERT_EQUALS( n.getNumChildren(), args.size() ); TS_ASSERT_EQUALS( n.getKind(), AND); - for( int i=0; i < args.size(); ++i ) { + for( unsigned i = 0; i < args.size(); ++i ) { TS_ASSERT_EQUALS( n[i], args[i]); } } @@ -145,7 +145,7 @@ public: Type* booleanType = d_nodeManager->booleanType(); Node x = d_nodeManager->mkVar(booleanType); TS_ASSERT_EQUALS(x.getKind(),VARIABLE); - TS_ASSERT_EQUALS(x.getNumChildren(),0); + TS_ASSERT_EQUALS(x.getNumChildren(),0u); TS_ASSERT_EQUALS(x.getType(),booleanType); } @@ -153,7 +153,7 @@ public: Type* booleanType = d_nodeManager->booleanType(); Node x = d_nodeManager->mkVar("x", booleanType); TS_ASSERT_EQUALS(x.getKind(),VARIABLE); - TS_ASSERT_EQUALS(x.getNumChildren(),0); + TS_ASSERT_EQUALS(x.getNumChildren(),0u); TS_ASSERT_EQUALS(x.getAttribute(VarNameAttr()),"x"); TS_ASSERT_EQUALS(x.getType(),booleanType); } @@ -219,7 +219,7 @@ public: TS_ASSERT( t->isFunction() ); FunctionType* ft = (FunctionType*)t; - TS_ASSERT_EQUALS(ft->getArgTypes().size(), 1); + TS_ASSERT_EQUALS(ft->getArgTypes().size(), 1u); TS_ASSERT_EQUALS(ft->getArgTypes()[0], booleanType); TS_ASSERT_EQUALS(ft->getRangeType(), booleanType); diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h index 28dbde933..9facd00f6 100644 --- a/test/unit/expr/node_white.h +++ b/test/unit/expr/node_white.h @@ -51,7 +51,7 @@ public: } void testNull() { - Node::s_null; + TS_ASSERT_EQUALS(Node::null(), Node::s_null); } void testCopyCtor() { -- cgit v1.2.3