diff --git a/configure.ac b/configure.ac index a02915ff4..a2e2d826d 100644 --- a/configure.ac +++ b/configure.ac @@ -101,15 +101,15 @@ AC_PROG_SED AS_IF([test "$CXX" = "g++"], [ # Enable OpenMP - CXXFLAGS+=" -fopenmp" - LDFLAGS+=" -fopenmp" - SLIBEXTRAFLAGS+=" -fopenmp" + CXXFLAGS="$CXXFLAGS -fopenmp" + LDFLAGS="$LDFLAGS -fopenmp" + SLIBEXTRAFLAGS="$SLIBEXTRAFLAGS -fopenmp" # Use -mfpmath=sse - CXXFLAGS+=" -mfpmath=sse" + CXXFLAGS="$CXXFLAGS -mfpmath=sse" ], [test "$CXX" = "clang++"], [ # OpenMP is not supported in clang++ - CXXFLAGS+=" -D _NO_OMP_" + CXXFLAGS="$CXXFLAGS -D _NO_OMP_" ], [ AC_MSG_ERROR([Unsupported compiler: $CXX]) @@ -128,28 +128,38 @@ host_os=`uname -s` AS_IF([test "$host_os" = "Darwin"], [ PLATFORM=osx SO_EXT=.dylib - SLIBFLAGS+="-dynamiclib" + SLIBFLAGS="$SLIBFLAGS -dynamiclib" COMP_VERSIONS="-compatibility_version \$(Z3_VERSION) -current_version \$(Z3_VERSION)" STATIC_FLAGS= ], [test "$host_os" = "Linux"], [ + CXXFLAGS=$CXXFLAGS -D _LINUX_ PLATFORM=linux SO_EXT=.so - LDFLAGS+=" -lrt" - SLIBFLAGS+=" -shared" + LDFLAGS="$LDFLAGS -lrt" + SLIBFLAGS="$SLIBFLAGS -shared" COMP_VERSIONS= STATIC_FLAGS=-static - CXXFLAGS+=" -fno-strict-aliasing" + CXXFLAGS="$CXXFLAGS -fno-strict-aliasing" if test "$CXX" = "clang++"; then # More flags for clang++ for Linux - CXXFLAGS+=" -Wno-unknown-pragmas -Wno-overloaded-virtual -Wno-unused-value" + CXXFLAGS="$CXXFLAGS -Wno-unknown-pragmas -Wno-overloaded-virtual -Wno-unused-value" fi - SLIBEXTRAFLAGS+=" -lrt" + SLIBEXTRAFLAGS="$SLIBEXTRAFLAGS -lrt" +], [test "$host_os" = "FreeBSD"], [ + CXXFLAGS="$CXXFLAGS -D _FREEBSD_" + PLATFORM=bsd + SO_EXT=.so + LDFLAGS="$LDFLAGS -lrt" + SLIBFLAGS="$SLIBFLAGS -shared" + COMP_VERSIONS= + STATIC_FLAGS=-static + SLIBEXTRAFLAGS="$SLIBEXTRAFLAGS -lrt" ], [test "${host_os:0:6}" = "CYGWIN"], [ PLATFORM=win SO_EXT=.dll - SLIBFLAGS+="-shared" + SLIBFLAGS="$SLIBFLAGS -shared" COMP_VERSIONS= - CXXFLAGS+=" -D_CYGWIN -fno-strict-aliasing" + CXXFLAGS="$CXXFLAGS -D_CYGWIN -fno-strict-aliasing" ], [ AC_MSG_ERROR([Unknown host platform: $host_os]) @@ -169,11 +179,11 @@ AC_CHECK_SIZEOF(int *) if test $ac_cv_sizeof_int_p -eq 8; then dnl In 64-bit systems we have to compile using -fPIC - CXXFLAGS+=" -fPIC" - CPPFLAGS+=" -D_AMD64_" + CXXFLAGS="$CXXFLAGS -fPIC" + CPPFLAGS="$CPPFLAGS -D_AMD64_" dnl Only enable use of thread local storage for 64-bit Linux. It is disabled for OSX and 32-bit Linux if test $PLATFORM = "linux"; then - CPPFLAGS+=" -D_USE_THREAD_LOCAL" + CPPFLAGS="$CPPFLAGS -D_USE_THREAD_LOCAL" fi IS_X64="yes" else diff --git a/src/tactic/fpa/fpa2bv_converter.h b/src/tactic/fpa/fpa2bv_converter.h index 09a1a4de2..291120e92 100644 --- a/src/tactic/fpa/fpa2bv_converter.h +++ b/src/tactic/fpa/fpa2bv_converter.h @@ -197,4 +197,4 @@ protected: void convert(model * bv_mdl, model * float_mdl); }; -#endif \ No newline at end of file +#endif diff --git a/src/tactic/fpa/qffpa_tactic.cpp b/src/tactic/fpa/qffpa_tactic.cpp index dd656666c..d034000c4 100644 --- a/src/tactic/fpa/qffpa_tactic.cpp +++ b/src/tactic/fpa/qffpa_tactic.cpp @@ -35,4 +35,4 @@ tactic * mk_qffpa_tactic(ast_manager & m, params_ref const & p) { using_params(mk_simplify_tactic(m, p), sat_simp_p), mk_sat_tactic(m, p), mk_fail_if_undecided_tactic()); -} \ No newline at end of file +} diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp index bde735a69..0fdb43b1f 100644 --- a/src/util/scoped_timer.cpp +++ b/src/util/scoped_timer.cpp @@ -33,15 +33,22 @@ Revision History: #include #include #include -#else +#elif defined(_LINUX_) || defined(_FREEBSD_) // Linux #include #include #include #include"warning.h" -#define CLOCKID CLOCK_PROCESS_CPUTIME_ID + #ifdef _LINUX_ + #define CLOCKID CLOCK_PROCESS_CPUTIME_ID + #else + // FreeBSD does not support CLOCK_PROCESS_CPUTIME_ID + #define CLOCKID CLOCK_PROF + #endif #define SIG SIGRTMIN // --------- +#else +// Other platforms #endif #include"scoped_timer.h" @@ -63,12 +70,14 @@ struct scoped_timer::imp { pthread_attr_t m_attributes; unsigned m_interval; pthread_cond_t m_condition_var; -#else - // Linux +#elif defined(_LINUX_) || defined(_FREEBSD_) + // Linux & FreeBSD static void * g_timer; void (*m_old_handler)(int); void * m_old_timer; timer_t m_timerid; +#else + // Other #endif #if defined(_WINDOWS) || defined(_CYGWIN) @@ -117,10 +126,12 @@ struct scoped_timer::imp { throw default_exception("failed to destroy pthread condition variable"); return st; } -#else +#elif defined(_LINUX_) static void sig_handler(int) { static_cast(g_timer)->m_eh->operator()(); } +#else + // Other #endif @@ -142,8 +153,8 @@ struct scoped_timer::imp { throw default_exception("failed to initialize timer thread attributes"); if (pthread_create(&m_thread_id, &m_attributes, &thread_func, this) != 0) throw default_exception("failed to start timer thread"); -#else - // Linux version +#elif defined(_LINUX_) || defined(_FREEBSD_) + // Linux & FreeBSD if (omp_in_parallel()) { // It doesn't work in with more than one thread. // SIGEV_SIGNAL: the event is handled by the process not by the thread that installed the handler. @@ -172,6 +183,8 @@ struct scoped_timer::imp { its.it_interval.tv_nsec = 0; if (timer_settime(m_timerid, 0, &its, NULL) == -1) throw default_exception("failed to set timer"); +#else + // Other platforms #endif } @@ -187,14 +200,16 @@ struct scoped_timer::imp { throw default_exception("failed to join thread"); if (pthread_attr_destroy(&m_attributes) != 0) throw default_exception("failed to destroy pthread attributes object"); -#else - // Linux version +#elif defined(_LINUX_) || defined(_FREEBSD_) + // Linux & FreeBSD if (omp_in_parallel()) return; // see comments in the constructor. timer_delete(m_timerid); if (m_old_handler != SIG_ERR) signal(SIG, m_old_handler); g_timer = m_old_timer; +#else + // Other Platforms #endif } @@ -203,9 +218,11 @@ struct scoped_timer::imp { #if defined(_WINDOWS) || defined(_CYGWIN) #elif defined(__APPLE__) && defined(__MACH__) // Mac OS X -#else -// Linux +#elif defined(_LINUX_) || defined(_FREEBSD_) +// Linux & FreeBSD void * scoped_timer::imp::g_timer = 0; +#else +// Other platforms #endif scoped_timer::scoped_timer(unsigned ms, event_handler * eh) {