fixed a number of problems with mac os x builds. build now works on mac os x if...

diff --git a/Makefile.builds.in b/Makefile.builds.in
index 83183e4a386102f0022be5fe21a652eb09acc6de..94f5235dbef8d9df2873b87182e0546fc8be79c8 100644 (file)
--- 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 ae681d2eb8d2113e57122fead09d701d761427e9..f22ae595a372d95b2ecc2f4f9361cf0079eea56c 100644 (file)
--- 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 01c40aca2c672da39cdab71cd682b1623e90573c..1435515ad34fe23015e218174647cefcaa7ab105 100644 (file)
--- 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 a005c7689e5c7b85de9cfeff01630814afa09269..f8c10c79f04d4e7e496ea890aa1c0c442a7b1eab 100644 (file)
--- 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 80eac93b0ffaab38a4ab7ddac6ab921af21c09a0..c2892d11c0024b0b9af9b30b540e5e0fd93a1c51 100644 (file)
--- 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 299e11deeff8a0045f7f9be009e25e71b98397b5..aa25ba9ebe18a20eb20710d5695a5e7fca034f46 100644 (file)
--- 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 64b1da51bc0997abfe823b3dc460aad4b22b1d45..6da3c08b52a48ab498ab278ea6206c89da0ee263 100644 (file)
--- 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);
   }