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)

3 files changed, 35 insertions, 4 deletions

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> */