fixed a number of problems with mac os x builds. build now works on mac os x if you disable the clock_gettime check in configure.ac (resolves bug #202), but the parser is broken (new bug #208)

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);
   }