Some fixes for GCC 4.2, and for Java on Mac

diff --git a/configure.ac b/configure.ac
index ca868c0d09f96c60334aa9540dd00af219b3f647..e860461b93eb451711972e5fa57acb9fe920c439 100644 (file)
--- a/configure.ac
+++ b/configure.ac
@@ -761,10 +761,26 @@ typedef pb_ds::priority_queue<void, void, void> pq;])],
     #include <ext/pb_ds/priority_queue.hpp>
     typedef __gnu_pbds::priority_queue<void, void, void> pq;])],
       [CVC4_PB_DS_NAMESPACE=__gnu_pbds],
-      [AC_MSG_ERROR([can't find required priority_queue in either __gnu_pbds or pb_ds namespace])])])
+      [AC_MSG_ERROR([cannot find required priority_queue in either __gnu_pbds or pb_ds namespace])])])
 AC_LANG_POP([C++])
-AC_DEFINE_UNQUOTED(CVC4_PB_DS_NAMESPACE, ${CVC4_PB_DS_NAMESPACE}, [The namespace for pb_ds data structures.])
 AC_MSG_RESULT([$CVC4_PB_DS_NAMESPACE])
+AC_DEFINE_UNQUOTED(CVC4_PB_DS_NAMESPACE, ${CVC4_PB_DS_NAMESPACE}, [The namespace for pb_ds data structures.])
+
+# for information: http://gcc.gnu.org/bugzilla/show_bug.cgi?id=36612
+AC_MSG_CHECKING([whether pb_ds has bug 36612])
+AC_LANG_PUSH([C++])
+AC_COMPILE_IFELSE([AC_LANG_SOURCE([
+#define __throw_container_error inline __throw_container_error
+#define __throw_insert_error inline __throw_insert_error
+#define __throw_join_error inline __throw_join_error
+#define __throw_resize_error inline __throw_resize_error
+#include <ext/pb_ds/exception.hpp>
+])],
+  [CVC4_GCC_HAS_PB_DS_BUG=1; bugverb=is],
+  [CVC4_GCC_HAS_PB_DS_BUG=0; bugverb="is not"])
+AC_LANG_POP([C++])
+AC_MSG_RESULT([bug $bugverb present])
+AC_DEFINE_UNQUOTED(CVC4_GCC_HAS_PB_DS_BUG, ${CVC4_GCC_HAS_PB_DS_BUG}, [Whether libstdc++ has a certain bug; see http://gcc.gnu.org/bugzilla/show_bug.cgi?id=36612])
 
 # Check for ANTLR runantlr script (defined in config/antlr.m4)
 AC_PROG_ANTLR
@@ -1123,6 +1139,13 @@ if test "$cvc4_build_java_bindings"; then
   fi
 fi
 
+# on Mac OS X, Java doesn't like the .so module extension; it wants .dylib
+module=no eval CVC4_JAVA_MODULE_EXT="$shrext_cmds"
+if test -z "$CVC4_JAVA_MODULE_EXT"; then
+  CVC4_JAVA_MODULE_EXT=.so
+fi
+AC_SUBST([CVC4_JAVA_MODULE_EXT])
+
 # Prepare configure output
 
 if test "$enable_shared" = yes; then BUILDING_SHARED=1; else BUILDING_SHARED=0; fi

diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am
index dcc4bc8580b2e493a4c465ee265b00214f179818..cc2a7c53fe265f1ecd593f6c6fe8792c5ede4e4c 100644 (file)
--- a/src/bindings/Makefile.am
+++ b/src/bindings/Makefile.am
@@ -60,6 +60,7 @@ javalib_LTLIBRARIES += java/libcvc4jni.la
 javadata_DATA += CVC4.jar
 java_libcvc4jni_la_LDFLAGS = \
        -module \
+       -shrext $(CVC4_JAVA_MODULE_EXT) \
        -version-info $(LIBCVC4BINDINGS_VERSION)
 java_libcvc4jni_la_LIBADD = \
        -L@builddir@/.. -lcvc4 \

diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h
index e616db3b91e51dbdf633f62034c056b4ea22f9bc..91d7e49eaba9ac15d7e0d247163f0c458cdd06a5 100644 (file)
--- a/src/theory/arith/error_set.h
+++ b/src/theory/arith/error_set.h
@@ -29,6 +29,22 @@
 
 #include "util/statistics_registry.h"
 //#include <boost/heap/d_ary_heap.hpp>
+
+#if CVC4_GCC_HAS_PB_DS_BUG
+   // Unfortunate bug in some older GCCs (e.g., v4.2):
+   //   http://gcc.gnu.org/bugzilla/show_bug.cgi?id=36612
+   // Requires some header-hacking to work around
+#  define __throw_container_error inline __throw_container_error
+#  define __throw_insert_error inline __throw_insert_error
+#  define __throw_join_error inline __throw_join_error
+#  define __throw_resize_error inline __throw_resize_error
+#  include <ext/pb_ds/exception.hpp>
+#  undef __throw_container_error
+#  undef __throw_insert_error
+#  undef __throw_join_error
+#  undef __throw_resize_error
+#endif /* CVC4_GCC_HAS_PB_DS_BUG */
+
 #include <ext/pb_ds/priority_queue.hpp>
 
 #include <vector>

diff --git a/test/system/Makefile.am b/test/system/Makefile.am
index e8e3f8c87c0eeef488898677aa8fd22815ada2b7..d79fcb7ba16f1cb200556d763e3dfc23f4cb5a8e 100644 (file)
--- a/test/system/Makefile.am
+++ b/test/system/Makefile.am
@@ -18,7 +18,9 @@ if CVC4_LANGUAGE_BINDING_JAVA
 TESTS += CVC4JavaTest.class
 endif
 
-CLASS_LOG_COMPILER = @srcdir@/run_java_test $(JAVA) -classpath .:@abs_top_builddir@/src/bindings/CVC4.jar -Djava.library.path=$(abs_top_builddir)/src/bindings/java/.libs:$(abs_top_builddir)/src/.libs
+# we set the DYLD_LIBRARY_PATH in addition to -Djava.library.path, seems
+# to be necessary on Mac
+CLASS_LOG_COMPILER = env DYLD_LIBRARY_PATH=$(abs_top_builddir)/src/bindings/java/.libs:$(abs_top_builddir)/src/.libs:$(abs_top_builddir)/src/parser/.libs @srcdir@/run_java_test $(JAVA) -classpath .:@abs_top_builddir@/src/bindings/CVC4.jar -Djava.library.path=$(abs_top_builddir)/src/bindings/java/.libs:$(abs_top_builddir)/src/.libs:$(abs_top_builddir)/src/parser/.libs
 
 # Things that aren't tests but that tests rely on and need to
 # go into the distribution

diff --git a/test/system/run_java_test b/test/system/run_java_test
index 205d869f2325d834c2754aa9cd1aa8cdf66cd94c..24947d52372505460ef08304848d46c1ef2e2725 100755 (executable)
--- a/test/system/run_java_test
+++ b/test/system/run_java_test
@@ -9,6 +9,6 @@
 # Works only for tests in the default package.
 #
 args=("$@")
-args[$((${#args}))]="$(echo "${args[${#args}]}" | sed 's,\(.*\/\)\?\(.*\)\.class$,\2,')"
+args[$((${#args}))]="$(echo "${args[${#args}]}" | sed 's,\(.*/\)*\(.*\)\.class$,\2,')"
 echo "${args[@]}"
 exec "${args[@]}"