From c3a6ff8c6e4a0c743cd33eb29931f837eeb2959e Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 8 Apr 2010 20:49:11 +0000 Subject: [PATCH] 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. --- Makefile.builds.in | 11 +-- configure.ac | 107 +++++++++++++++++++-------- src/Makefile.am | 4 - test/unit/Makefile.am | 8 +- test/unit/context/cdlist_black.h | 10 +-- test/unit/context/context_mm_black.h | 38 +++++----- 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 +- test/unit/theory/theory_black.h | 2 +- test/unit/theory/theory_uf_white.h | 2 +- test/unit/util/integer_black.h | 28 +++---- test/unit/util/integer_white.h | 8 +- test/unit/util/rational_white.h | 28 +++---- 16 files changed, 198 insertions(+), 158 deletions(-) diff --git a/Makefile.builds.in b/Makefile.builds.in index 1cf9c1a52..9dd9a314a 100644 --- a/Makefile.builds.in +++ b/Makefile.builds.in @@ -30,10 +30,11 @@ bindir = @bindir@ libdir = @libdir@ abs_builddir = @abs_builddir@ -# Are we building static/dynamic libraries? One or the other can be +# Are we building static/dynamic libraries/binaries? One or the other can be # on, or both. BUILDING_STATIC = @BUILDING_STATIC@ BUILDING_SHARED = @BUILDING_SHARED@ +STATIC_BINARY = @STATIC_BINARY@ .PHONY: _default_build_ all _default_build_: all @@ -51,8 +52,8 @@ all: $(CURRENT_BUILD)/libtool --mode=install install -v \ $(CURRENT_BUILD)/src/parser/libcvc4parser.la \ "$(abs_builddir)$(libdir)" -ifeq ($(BUILDING_SHARED),1) -# if we're building shared libs, relink +ifeq ($(BUILDING_SHARED)$(STATIC_BINARY),10) +# if we're building shared libs and the binary is not static, relink thelibdir="$(abs_builddir)$(libdir)"; \ progdir="$(abs_builddir)$(bindir)"; file=cvc4; \ eval `grep '^relink_command=' $(CURRENT_BUILD)/src/main/cvc4 | sed 's:-Wl,-rpath:-Wl,-rpath -Wl,\\\\$$thelibdir -Wl,-rpath:'`; \ @@ -72,8 +73,8 @@ endif $(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/libcvc4.la "`pwd`$(libdir)" # install libcvc4parser $(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/parser/libcvc4parser.la "`pwd`$(libdir)" -ifeq ($(BUILDING_SHARED),1) -# if we're building shared libs, relink +ifeq ($(BUILDING_SHARED)$(STATIC_BINARY),10) +# if we're building shared libs and the binary is not static, relink thelibdir="`pwd`$(libdir)"; progdir="`pwd`$(bindir)"; file=cvc4; \ eval `grep '^relink_command=' $(CURRENT_BUILD)/src/main/cvc4 | sed 's:-Wl,-rpath:-Wl,-rpath -Wl,\\\\$$thelibdir -Wl,-rpath:'`; \ eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)" diff --git a/configure.ac b/configure.ac index d23cf4a6d..a44dc4b66 100644 --- a/configure.ac +++ b/configure.ac @@ -50,6 +50,10 @@ CVC4_PARSER_LIBRARY_VERSION=$CVC4_MAJOR:$CVC4_MINOR:$CVC4_RELEASE # some things.) config_cmdline="$@" +# remember if the user set these explicitly (or whether autoconf does) +user_specified_enable_or_disable_static=${enable_static+yes} +user_specified_enable_or_disable_shared=${enable_shared+yes} + # turn off static lib building by default AC_ENABLE_SHARED AC_DISABLE_STATIC @@ -157,7 +161,24 @@ elif test -e src/include/cvc4_public.h; then cd "builds/$target/$build_type" CVC4_CONFIGURE_IN_BUILDS=yes; export CVC4_CONFIGURE_IN_BUILDS echo ../../../configure $config_cmdline - exec ../../../configure $config_cmdline + `pwd`/../../../configure $config_cmdline + exitval=$? + cd ../../.. + if test $exitval -eq 0; then + cat >config.status <::const_iterator j = list.begin(); j != list.end(); ++j) { - TS_ASSERT(*j == i2++); + TS_ASSERT_EQUALS(*j, i2++); } } - TS_ASSERT(list.size() == N); + TS_ASSERT_EQUALS(list.size(), unsigned(N)); for(int i = 0; i < N; ++i) { - TS_ASSERT(list[i] == i); + TS_ASSERT_EQUALS(list[i], i); } } diff --git a/test/unit/context/context_mm_black.h b/test/unit/context/context_mm_black.h index bda1cb141..e25d1f336 100644 --- a/test/unit/context/context_mm_black.h +++ b/test/unit/context/context_mm_black.h @@ -10,7 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** Black box testing of CVC4::Node. + ** Black box testing of CVC4::context::ContextMemoryManager. **/ #include @@ -40,23 +40,24 @@ public: // Push, then allocate, then pop // We make sure that we don't allocate too much so that all the regions // should be reclaimed - int chunkSizeBytes = 16384; - int maxFreeChunks = 100; - int piecesPerChunk = 13; - int len = chunkSizeBytes / piecesPerChunk; // Length of the individual block - int N = maxFreeChunks*piecesPerChunk; - for (int p = 0; p < 5; ++ p) { + unsigned chunkSizeBytes = 16384; + unsigned maxFreeChunks = 100; + unsigned piecesPerChunk = 13; + unsigned len = chunkSizeBytes / piecesPerChunk; // Length of the individual block + unsigned N = maxFreeChunks*piecesPerChunk; + for(unsigned p = 0; p < 5; ++ p) { d_cmm->push(); - for (int i = 0; i < N; ++i) { + for(unsigned i = 0; i < N; ++i) { char* newMem = (char*)d_cmm->newData(len); // We only setup the memory in the first run, the others should // reclaim the same memory - if (p == 0) { - for(int k = 0; k < len - 1; k ++) + if(p == 0) { + for(unsigned k = 0; k < len - 1; k ++) { newMem[k] = 'a'; + } newMem[len-1] = 0; } - if (strlen(newMem) != len - 1) { + if(strlen(newMem) != len - 1) { cout << strlen(newMem) << " : " << len - 1 << endl; } TS_ASSERT(strlen(newMem) == len - 1); @@ -64,22 +65,23 @@ public: d_cmm->pop(); } - int factor = 3; - N = 16384/factor; + unsigned factor = 3; + N = 16384 / factor; // Push, then allocate, then pop all at once - for (int p = 0; p < 5; ++ p) { + for(unsigned p = 0; p < 5; ++ p) { d_cmm->push(); - for (int i = 1; i < N; ++i) { - int len = i*factor; + for(unsigned i = 1; i < N; ++i) { + unsigned len = i * factor; char* newMem = (char*)d_cmm->newData(len); - for(int k = 0; k < len - 1; k ++) + for(unsigned k = 0; k < len - 1; k ++) { newMem[k] = 'a'; + } newMem[len-1] = 0; TS_ASSERT(strlen(newMem) == len - 1); } } - for (int p = 0; p < 5; ++ p) { + for(unsigned p = 0; p < 5; ++ p) { d_cmm->pop(); } 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() { diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 905294c27..24c8e407c 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -228,7 +228,7 @@ public: TS_ASSERT_EQUALS(got, f_x_eq_x); - TS_ASSERT_EQUALS(5, d_dummy->d_registered.size()); + TS_ASSERT_EQUALS(5u, d_dummy->d_registered.size()); TS_ASSERT(d_dummy->d_registered.find(x) != d_dummy->d_registered.end()); TS_ASSERT(d_dummy->d_registered.find(f) != d_dummy->d_registered.end()); TS_ASSERT(d_dummy->d_registered.find(f_x) != d_dummy->d_registered.end()); diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h index 369be5a16..c02214a25 100644 --- a/test/unit/theory/theory_uf_white.h +++ b/test/unit/theory/theory_uf_white.h @@ -145,7 +145,7 @@ public: d_euf->assertFact( f5_x_eq_x ); d_euf->check(d_level); - TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls()); + TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls()); TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0)); Node realConflict = d_outputChannel.getIthNode(0); TS_ASSERT_EQUALS(expectedConflict, realConflict); diff --git a/test/unit/util/integer_black.h b/test/unit/util/integer_black.h index afd2145e3..c09db2207 100644 --- a/test/unit/util/integer_black.h +++ b/test/unit/util/integer_black.h @@ -45,16 +45,16 @@ public: TS_ASSERT_EQUALS(z4.getLong(), 0); Integer z5("7896890"); - TS_ASSERT_EQUALS(z5.getUnsignedLong(), 7896890); + TS_ASSERT_EQUALS(z5.getUnsignedLong(), 7896890ul); Integer z6(z5); - TS_ASSERT_EQUALS(z5.getUnsignedLong(), 7896890); - TS_ASSERT_EQUALS(z6.getUnsignedLong(), 7896890); + TS_ASSERT_EQUALS(z5.getUnsignedLong(), 7896890ul); + TS_ASSERT_EQUALS(z6.getUnsignedLong(), 7896890ul); string bigValue("1536729"); Integer z7(bigValue); - TS_ASSERT_EQUALS(z7.getUnsignedLong(), 1536729); + TS_ASSERT_EQUALS(z7.getUnsignedLong(), 1536729ul); } void testOperatorAssign(){ @@ -62,24 +62,24 @@ public: Integer y(79); Integer z(45789); - TS_ASSERT_EQUALS(x.getUnsignedLong(), 0); - TS_ASSERT_EQUALS(y.getUnsignedLong(), 79); - TS_ASSERT_EQUALS(z.getUnsignedLong(), 45789); + TS_ASSERT_EQUALS(x.getUnsignedLong(), 0ul); + TS_ASSERT_EQUALS(y.getUnsignedLong(), 79ul); + TS_ASSERT_EQUALS(z.getUnsignedLong(), 45789ul); x = y = z; - TS_ASSERT_EQUALS(x.getUnsignedLong(), 45789); - TS_ASSERT_EQUALS(y.getUnsignedLong(), 45789); - TS_ASSERT_EQUALS(z.getUnsignedLong(), 45789); + TS_ASSERT_EQUALS(x.getUnsignedLong(), 45789ul); + TS_ASSERT_EQUALS(y.getUnsignedLong(), 45789ul); + TS_ASSERT_EQUALS(z.getUnsignedLong(), 45789ul); Integer a(2); y = a; - TS_ASSERT_EQUALS(a.getUnsignedLong(), 2); - TS_ASSERT_EQUALS(y.getUnsignedLong(), 2); - TS_ASSERT_EQUALS(x.getUnsignedLong(), 45789); - TS_ASSERT_EQUALS(z.getUnsignedLong(), 45789); + TS_ASSERT_EQUALS(a.getUnsignedLong(), 2ul); + TS_ASSERT_EQUALS(y.getUnsignedLong(), 2ul); + TS_ASSERT_EQUALS(x.getUnsignedLong(), 45789ul); + TS_ASSERT_EQUALS(z.getUnsignedLong(), 45789ul); } void testOperatorEquals(){ diff --git a/test/unit/util/integer_white.h b/test/unit/util/integer_white.h index ef0e0b92f..3a86289a3 100644 --- a/test/unit/util/integer_white.h +++ b/test/unit/util/integer_white.h @@ -33,9 +33,9 @@ public: Integer fits_in_16_bytes("7890D789D33234027890D789D3323402", 16); - TS_ASSERT_THROWS_NOTHING(size_t res0 = zero.hash()); - TS_ASSERT_THROWS_NOTHING(size_t res1 = fits_in_2_bytes.hash()); - TS_ASSERT_THROWS_NOTHING(size_t res2 = fits_in_16_bytes.hash()); - TS_ASSERT_THROWS_NOTHING(size_t res3 = large.hash()); + TS_ASSERT_THROWS_NOTHING(zero.hash()); + TS_ASSERT_THROWS_NOTHING(fits_in_2_bytes.hash()); + TS_ASSERT_THROWS_NOTHING(fits_in_16_bytes.hash()); + TS_ASSERT_THROWS_NOTHING(large.hash()); } }; diff --git a/test/unit/util/rational_white.h b/test/unit/util/rational_white.h index 559b457cb..8a7f04fd3 100644 --- a/test/unit/util/rational_white.h +++ b/test/unit/util/rational_white.h @@ -104,26 +104,26 @@ public: Rational y(78,6); Rational z(45789,1); - TS_ASSERT_EQUALS(x.getNumerator().getUnsignedLong(), 0); - TS_ASSERT_EQUALS(y.getNumerator().getUnsignedLong(), 13); - TS_ASSERT_EQUALS(z.getNumerator().getUnsignedLong(), 45789); + TS_ASSERT_EQUALS(x.getNumerator().getUnsignedLong(), 0ul); + TS_ASSERT_EQUALS(y.getNumerator().getUnsignedLong(), 13ul); + TS_ASSERT_EQUALS(z.getNumerator().getUnsignedLong(), 45789ul); x = y = z; - TS_ASSERT_EQUALS(x.getNumerator().getUnsignedLong(), 45789); - TS_ASSERT_EQUALS(y.getNumerator().getUnsignedLong(), 45789); - TS_ASSERT_EQUALS(z.getNumerator().getUnsignedLong(), 45789); + TS_ASSERT_EQUALS(x.getNumerator().getUnsignedLong(), 45789ul); + TS_ASSERT_EQUALS(y.getNumerator().getUnsignedLong(), 45789ul); + TS_ASSERT_EQUALS(z.getNumerator().getUnsignedLong(), 45789ul); Rational a(78,91); y = a; - TS_ASSERT_EQUALS(a.getNumerator().getUnsignedLong(), 6); - TS_ASSERT_EQUALS(a.getDenominator().getUnsignedLong(), 7); - TS_ASSERT_EQUALS(y.getNumerator().getUnsignedLong(), 6); - TS_ASSERT_EQUALS(y.getDenominator().getUnsignedLong(), 7); - TS_ASSERT_EQUALS(x.getNumerator().getUnsignedLong(), 45789); - TS_ASSERT_EQUALS(z.getNumerator().getUnsignedLong(), 45789); + TS_ASSERT_EQUALS(a.getNumerator().getUnsignedLong(), 6ul); + TS_ASSERT_EQUALS(a.getDenominator().getUnsignedLong(), 7ul); + TS_ASSERT_EQUALS(y.getNumerator().getUnsignedLong(), 6ul); + TS_ASSERT_EQUALS(y.getDenominator().getUnsignedLong(), 7ul); + TS_ASSERT_EQUALS(x.getNumerator().getUnsignedLong(), 45789ul); + TS_ASSERT_EQUALS(z.getNumerator().getUnsignedLong(), 45789ul); } void testToStringStuff(){ @@ -416,8 +416,8 @@ public: Rational one_word(75890L,590L); Rational two_words("7890D789D33234027890D789D3323402", 16); - TS_ASSERT_EQUALS(zero.hash(), 1); - TS_ASSERT_EQUALS(one_word.hash(), 7589 xor 59); + TS_ASSERT_EQUALS(zero.hash(), 1u); + TS_ASSERT_EQUALS(one_word.hash(), 7589u xor 59u); TS_ASSERT_EQUALS(two_words.hash(), (two_words.getNumerator().hash()) xor 1); TS_ASSERT_EQUALS(large.hash(), -- 2.30.2