From e070c4a6d716407916c65a66ea9f019d1681ae8e Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 29 Apr 2013 18:03:28 -0400 Subject: [PATCH] Some fixes for GCC 4.2, and for Java on Mac --- configure.ac | 27 +++++++++++++++++++++++++-- src/bindings/Makefile.am | 1 + src/theory/arith/error_set.h | 16 ++++++++++++++++ test/system/Makefile.am | 4 +++- test/system/run_java_test | 2 +- 5 files changed, 46 insertions(+), 4 deletions(-) diff --git a/configure.ac b/configure.ac index ca868c0d0..e860461b9 100644 --- a/configure.ac +++ b/configure.ac @@ -761,10 +761,26 @@ typedef pb_ds::priority_queue pq;])], #include typedef __gnu_pbds::priority_queue 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 +])], + [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 dcc4bc858..cc2a7c53f 100644 --- 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 e616db3b9..91d7e49ea 100644 --- a/src/theory/arith/error_set.h +++ b/src/theory/arith/error_set.h @@ -29,6 +29,22 @@ #include "util/statistics_registry.h" //#include + +#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 +# undef __throw_container_error +# undef __throw_insert_error +# undef __throw_join_error +# undef __throw_resize_error +#endif /* CVC4_GCC_HAS_PB_DS_BUG */ + #include #include diff --git a/test/system/Makefile.am b/test/system/Makefile.am index e8e3f8c87..d79fcb7ba 100644 --- 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 205d869f2..24947d523 100755 --- 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[@]}" -- 2.30.2