Modify LDFLAGS to support shared libraries for Win (#1280)

* Use uintptr_t for pointer casts in Swig files

CVC4's Swig interface files were casting pointers to longs in multiple
instances. The problem with that is that on certain platforms *cough*
Windows/MinGW *cough* long is only 32-bit even when compiling a 64-bit
executable (they use the LLP64 data model). This made the compilation of
language bindings fail with MinGW. This commit changes the types to
uintptr_t defined in Swig's stdint.i.

* Modify LDFLAGS to support shared libraries for Win

This commit adds "-no-undefined" to the LDFLAGS of CVC4's library, which
is required for building DLLs (shared libraries on Windows). It also
adds "--export-all-symbols" to the linker flags of the parser to ensure
that there are no unresolved symbols when linking against it (see
comment in the Makefile.am for details).

* Fix for non-Windows builds

* add no-undefined to libcvc4compatjni

diff --git a/configure.ac b/configure.ac
index 85660f223c8e2795798a3701426bae00b90abeb1..cb36c7a9dbe89407f1560a9645b555ea7de2ec38 100644 (file)
--- a/configure.ac
+++ b/configure.ac
@@ -1305,12 +1305,16 @@ LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
 
 # visibility flag not supported for Windows builds
 # also increase default stack size for Windows binaries
+windows_build=no
 case $host_os in
   (*mingw*) FLAG_VISIBILITY_HIDDEN=
             cvc4_LDFLAGS=-Wl,--stack,134217728
             pcvc4_LDFLAGS=-Wl,--stack,134217728
+            windows_build=yes
 esac
 
+AM_CONDITIONAL([CVC4_WINDOWS_BUILD], [test "$windows_build" = "yes"])
+
 AC_SUBST(FLAG_VISIBILITY_HIDDEN)
 AC_SUBST(cvc4_LDFLAGS)
 AC_SUBST(pcvc4_LDFLAGS)

diff --git a/src/Makefile.am b/src/Makefile.am
index 7f9d5a84bbafb27d7725cb3bac4bfb5d654638c2..b05a3503c46e77c9a0c132b83f5e9f5f4e84a320 100644 (file)
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -25,7 +25,9 @@ include @top_srcdir@/src/Makefile.theories
 
 lib_LTLIBRARIES = libcvc4.la
 
-libcvc4_la_LDFLAGS = -no-undefined -version-info $(LIBCVC4_VERSION)
+libcvc4_la_LDFLAGS = \
+       -no-undefined \
+       -version-info $(LIBCVC4_VERSION)
 
 # This "tricks" automake into linking us as a C++ library (rather than
 # as a C library, which messes up exception handling support)

diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am
index e7548bbe143a835f1dc42c41e73f6c4ef6ccf62a..99405488206ef380fbedb621b35c504bf67eeae9 100644 (file)
--- a/src/bindings/Makefile.am
+++ b/src/bindings/Makefile.am
@@ -59,6 +59,7 @@ if CVC4_LANGUAGE_BINDING_JAVA
 javalib_LTLIBRARIES += java/libcvc4jni.la
 javadata_DATA += CVC4.jar
 java_libcvc4jni_la_LDFLAGS = \
+       -no-undefined \
        -module \
        -shrext $(CVC4_JAVA_MODULE_EXT) \
        -version-info $(LIBCVC4BINDINGS_VERSION)

diff --git a/src/bindings/compat/java/Makefile.am b/src/bindings/compat/java/Makefile.am
index 5b052568d266e40d9e064081cc479d06d3f0fd09..eae498368fc3e2f66c659f4c97fd200ee228d01d 100644 (file)
--- a/src/bindings/compat/java/Makefile.am
+++ b/src/bindings/compat/java/Makefile.am
@@ -29,6 +29,7 @@ if CVC4_LANGUAGE_BINDING_JAVA
 javalib_LTLIBRARIES += libcvc4compatjni.la
 javadata_DATA += CVC4compat.jar
 libcvc4compatjni_la_LDFLAGS = \
+       -no-undefined \
        -module \
        -shrext $(CVC4_JAVA_MODULE_EXT) \
        -version-info $(LIBCVC4BINDINGS_VERSION)

diff --git a/src/compat/Makefile.am b/src/compat/Makefile.am
index df4603a9a320c0e034cf0d4dd38de66e770a5ca5..47c8a6a9809b407928899e83bcf9e8a281f8b1fb 100644 (file)
--- a/src/compat/Makefile.am
+++ b/src/compat/Makefile.am
@@ -22,6 +22,7 @@ if CVC4_BUILD_LIBCOMPAT
 lib_LTLIBRARIES = libcvc4compat.la
 
 libcvc4compat_la_LDFLAGS = \
+       -no-undefined \
        -version-info $(LIBCVC4COMPAT_VERSION)
 
 libcvc4compat_la_LIBADD = \

diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index a316019fd82b649175fbbb36dc996067fe3e247e..98b98ccaf4714934f644e2f43fa464f3c839a986 100644 (file)
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -21,9 +21,20 @@ SUBDIRS = smt1 smt2 cvc tptp
 
 lib_LTLIBRARIES = libcvc4parser.la
 
-libcvc4parser_la_LDFLAGS = $(ANTLR_LDFLAGS) \
+libcvc4parser_la_LDFLAGS = \
+       $(ANTLR_LDFLAGS) \
+       -no-undefined \
        -version-info $(LIBCVC4PARSER_VERSION)
 
+if CVC4_WINDOWS_BUILD
+# -Wl,--export-all-symbols makes sure that all symbols are exported when
+# building a DLL. This option is on by default but gets disabled for the parser
+# library because the generated lexer/parser files define some functions as
+# __declspec(dllexport), which leads to lots of unresolved symbols when linking
+# against libcvc4parser.
+libcvc4parser_la_LDFLAGS += -Wl,--export-all-symbols
+endif
+
 libcvc4parser_la_LIBADD = \
        @builddir@/smt1/libparsersmt1.la \
        @builddir@/smt2/libparsersmt2.la \