diff options
-rw-r--r-- | Makefile.builds.in | 26 | ||||
-rw-r--r-- | configure.ac | 4 | ||||
-rw-r--r-- | src/util/Assert.cpp | 2 | ||||
-rw-r--r-- | src/util/stats.h | 35 | ||||
-rw-r--r-- | src/util/tls.h.in | 2 | ||||
-rw-r--r-- | test/unit/context/cdlist_black.h | 11 | ||||
-rw-r--r-- | test/unit/memory.h | 12 |
7 files changed, 83 insertions, 9 deletions
diff --git a/Makefile.builds.in b/Makefile.builds.in index 83183e4a3..94f5235db 100644 --- a/Makefile.builds.in +++ b/Makefile.builds.in @@ -54,10 +54,21 @@ all: "$(abs_builddir)$(libdir)" ifeq ($(BUILDING_SHARED)$(STATIC_BINARY),10) # if we're building shared libs and the binary is not static, relink +# the handling with empty $relink_command is a hack for Mac OS 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:'`; \ - eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)" + if test -z "$$relink_command"; then \ + $(mkinstalldirs) "$(CURRENT_BUILD)$(bindir)/.libs"; \ + $(install_sh) \ + $(CURRENT_BUILD)/src/main/.libs/cvc4 \ + "$(abs_builddir)$(bindir)/.libs"; \ + $(install_sh) \ + $(CURRENT_BUILD)/src/main/cvc4 \ + "$(abs_builddir)$(bindir)"; \ + else \ + eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)"; \ + fi else # if we're building static libs only, just install the driver binary directly $(install_sh) \ @@ -75,9 +86,20 @@ endif $(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/parser/libcvc4parser.la "`pwd`$(libdir)" ifeq ($(BUILDING_SHARED)$(STATIC_BINARY),10) # if we're building shared libs and the binary is not static, relink +# the handling with empty $relink_command is a hack for Mac OS 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)" + if test -z "$$relink_command"; then \ + $(mkinstalldirs) ".$(bindir)/.libs"; \ + $(install_sh) \ + $(CURRENT_BUILD)/src/main/.libs/cvc4 \ + "`pwd`$(bindir)/.libs"; \ + $(install_sh) \ + $(CURRENT_BUILD)/src/main/cvc4 \ + "`pwd`$(bindir)"; \ + else \ + eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)"; \ + fi else # if we're building static libs only, just install the driver binary directly $(install_sh) $(CURRENT_BUILD)/src/main/cvc4 "`pwd`$(bindir)" diff --git a/configure.ac b/configure.ac index ae681d2eb..f22ae595a 100644 --- a/configure.ac +++ b/configure.ac @@ -300,11 +300,11 @@ elif test "$CVC4_CONFIGURE_AT_TOP_LEVEL" = yes; then cat >config.reconfig <<EOF [#!/bin/bash # Generated by configure, `date` -# This script part of CVC4. +# This script is part of CVC4. cd "\`dirname \\"\$0\\"\`" -current=(\`grep '^CURRENT_BUILD' builds/current | sed 's,^CURRENT_BUILD *= *\([^/]\\+\\)/\\(.*\\),\\1 \\2,'\`) +current=(\`grep '^CURRENT_BUILD' builds/current | sed 's,^CURRENT_BUILD *= *\([^/]*\\)/\\(.*\\),\\1 \\2,'\`) arch=\${current[0]} build=\${current[1]} diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp index 01c40aca2..1435515ad 100644 --- a/src/util/Assert.cpp +++ b/src/util/Assert.cpp @@ -138,7 +138,7 @@ void AssertionException::construct(const char* header, const char* extra, */ void debugAssertionFailed(const AssertionException& thisException, const char* propagatingException) { - static __thread bool alreadyFired = false; + static CVC4_THREADLOCAL(bool) alreadyFired = false; if(EXPECT_TRUE( !std::uncaught_exception() ) || alreadyFired) { throw thisException; diff --git a/src/util/stats.h b/src/util/stats.h index a005c7689..f8c10c79f 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -310,6 +310,36 @@ inline std::ostream& operator<<(std::ostream& os, const ::timespec& t) { } +#ifdef __APPLE__ + +class TimerStat : public BackedStat< ::timespec > { + bool d_running; + +public: + + TimerStat(const std::string& s) : + BackedStat< ::timespec >(s, ::timespec()), + d_running(false) { + } + + void start() { + if(__CVC4_USE_STATISTICS) { + AlwaysAssert(!d_running); + d_running = true; + } + } + + void stop() { + if(__CVC4_USE_STATISTICS) { + AlwaysAssert(d_running); + ++d_data.tv_sec; + d_running = false; + } + } +};/* class TimerStat */ + +#else /* __APPLE__ */ + class TimerStat : public BackedStat< ::timespec > { // strange: timespec isn't placed in 'std' namespace ?! ::timespec d_start; @@ -325,7 +355,7 @@ public: void start() { if(__CVC4_USE_STATISTICS) { AlwaysAssert(!d_running); - clock_gettime(CLOCK_REALTIME, &d_start); + clock_gettime(CLOCK_MONOTONIC, &d_start); d_running = true; } } @@ -334,13 +364,14 @@ public: if(__CVC4_USE_STATISTICS) { AlwaysAssert(d_running); ::timespec end; - clock_gettime(CLOCK_REALTIME, &end); + clock_gettime(CLOCK_MONOTONIC, &end); d_data += end - d_start; d_running = false; } } };/* class TimerStat */ +#endif /* __APPLE__ */ #undef __CVC4_USE_STATISTICS diff --git a/src/util/tls.h.in b/src/util/tls.h.in index 80eac93b0..c2892d11c 100644 --- a/src/util/tls.h.in +++ b/src/util/tls.h.in @@ -71,7 +71,7 @@ public: } operator T() const { - return reinterpret_cast<T>(pthread_getspecific(d_key)); + return static_cast<T>(pthread_getspecific(d_key)); } };/* class ThreadLocalImpl<T, true> */ diff --git a/test/unit/context/cdlist_black.h b/test/unit/context/cdlist_black.h index 299e11dee..aa25ba9eb 100644 --- a/test/unit/context/cdlist_black.h +++ b/test/unit/context/cdlist_black.h @@ -133,9 +133,16 @@ public: TS_ASSERT_EQUALS(aThirdFalse, false); } + /* setrlimit() totally broken on Mac OS X */ void testOutOfMemory() { +#ifdef __APPLE__ + + TS_WARN("can't run memory tests on Mac OS X"); + +#else /* __APPLE__ */ + CDList<unsigned> list(d_context); - WithLimitedMemory wlm(0); + WithLimitedMemory wlm(1); TS_ASSERT_THROWS({ // We cap it at UINT_MAX, preferring to terminate with a @@ -144,5 +151,7 @@ public: list.push_back(i); } }, bad_alloc); + +#endif /* __APPLE__ */ } }; diff --git a/test/unit/memory.h b/test/unit/memory.h index 64b1da51b..6da3c08b5 100644 --- a/test/unit/memory.h +++ b/test/unit/memory.h @@ -31,6 +31,8 @@ #include <sys/time.h> #include <sys/resource.h> +#include "util/Assert.h" + namespace CVC4 { namespace test { @@ -46,10 +48,20 @@ class WithLimitedMemory { public: WithLimitedMemory() { +#ifdef __APPLE__ + TS_FAIL("setrlimit() is broken on Mac, can't run memory tests."); + AlwaysAssert(false, + "setrlimit() is broken on Mac, can't run memory tests."); +#endif /* __APPLE__ */ remember(); } WithLimitedMemory(rlim_t amount) { +#ifdef __APPLE__ + TS_FAIL("setrlimit() is broken on Mac, can't run memory tests."); + AlwaysAssert(false, + "setrlimit() is broken on Mac, can't run memory tests."); +#endif /* __APPLE__ */ remember(); set(amount); } |