diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-25 18:57:48 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-25 18:57:48 +0000 |
commit | 94b685e149119bbe75266481f6de3a0915e7c10a (patch) | |
tree | addbbdd36ca34f65c7d3d092c0f1fc5d400c6dac /configure.ac | |
parent | 89bcd4deee07a2c61d30a9dfca64e58e8c2d701b (diff) |
fix some Mac issues
Diffstat (limited to 'configure.ac')
-rw-r--r-- | configure.ac | 21 |
1 files changed, 20 insertions, 1 deletions
diff --git a/configure.ac b/configure.ac index 3ef0ac689..30284b3f9 100644 --- a/configure.ac +++ b/configure.ac @@ -407,7 +407,7 @@ case "$with_build" in if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi ;; debug) # unoptimized, debug symbols, assertions, tracing, dumping - CVC4CPPFLAGS=-DCVC4_DEBUG + CVC4CPPFLAGS='-DCVC4_DEBUG' CVC4CXXFLAGS='-fno-inline' CVC4CFLAGS='-fno-inline' CVC4LDFLAGS= @@ -709,6 +709,25 @@ namespace __gnu_cxx { template<> struct hash<uint64_t> {}; }])], [AC_MSG_RESULT([yes])]) AC_LANG_POP([C++]) +# Check whether "long" and "int64_t" are distinct types w.r.t. overloading. +# Even if they have the same size, they can be distinct, and some platforms +# can have problems with ambiguous function calls when auto-converting +# int64_t to long, and others will complain if you overload a function +# that takes an int64_t with one that takes a long (giving a redefinition +# error). So we have to keep both happy. Probably the same underlying +# issue as the hash specialization above, but let's check separately +# for flexibility. +AC_MSG_CHECKING([for the relationship between long and int64_t]) +AC_LANG_PUSH([C++]) +AC_COMPILE_IFELSE([AC_LANG_SOURCE([ +#include <stdint.h> +void foo(long); +void foo(int64_t);])], + [AC_MSG_RESULT([no relationship detected]); CVC4_NEED_INT64_T_OVERLOADS=1], + [AC_MSG_RESULT([typedef or similar]); CVC4_NEED_INT64_T_OVERLOADS=0]) +AC_LANG_POP([C++]) +AC_SUBST([CVC4_NEED_INT64_T_OVERLOADS]) + # Check for ANTLR runantlr script (defined in config/antlr.m4) AC_PROG_ANTLR |