more build system fix-ups

diff --git a/src/Makefile.am b/src/Makefile.am
index 110ab985584cb58a8231ba1facfc23dda0819f78..97a2eceadeabca5ea50b931a62268cdd4cd85f9f 100644 (file)
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -27,11 +27,15 @@ lib_LTLIBRARIES = libcvc4.la
 noinst_LTLIBRARIES = libcvc4_noinst.la
 
 libcvc4_la_LDFLAGS = -version-info $(LIBCVC4_VERSION) -release $(LIBCVC4_RELEASE)
+libcvc4_la_LINK = $(CXXLINK)
 
 libcvc4_la_SOURCES =
 libcvc4_la_LIBADD = libcvc4_noinst.la
 
-libcvc4_noinst_la_SOURCES =
+# empty.cpp is a fake file added to "trick" automake into linking us as a
+# C++ library (rather than as a C library, which messes up exception
+# handling support)
+libcvc4_noinst_la_SOURCES = empty.cpp
 libcvc4_noinst_la_LIBADD = \
        @builddir@/util/libutil.la \
        @builddir@/expr/libexpr.la \
@@ -41,6 +45,9 @@ libcvc4_noinst_la_LIBADD = \
        @builddir@/smt/libsmt.la \
        @builddir@/theory/libtheory.la
 
+# empty.cpp hack; see above
+empty.cpp:; touch empty.cpp
+
 publicheaders = \
        include/cvc4_config.h
 

diff --git a/src/Makefile.in b/src/Makefile.in
index c650c15033509066ebd025a62958dfc533a991d1..9099b92beba7c2d55dae5b2078c0bf2588b66b72 100644 (file)
--- a/src/Makefile.in
+++ b/src/Makefile.in
@@ -76,17 +76,26 @@ LTLIBRARIES = $(lib_LTLIBRARIES) $(noinst_LTLIBRARIES)
 libcvc4_la_DEPENDENCIES = libcvc4_noinst.la
 am_libcvc4_la_OBJECTS =
 libcvc4_la_OBJECTS = $(am_libcvc4_la_OBJECTS)
-libcvc4_la_LINK = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) \
-       $(LIBTOOLFLAGS) --mode=link $(CCLD) $(AM_CFLAGS) $(CFLAGS) \
-       $(libcvc4_la_LDFLAGS) $(LDFLAGS) -o $@
 libcvc4_noinst_la_DEPENDENCIES = @builddir@/util/libutil.la \
        @builddir@/expr/libexpr.la @builddir@/context/libcontext.la \
        @builddir@/prop/libprop.la \
        @builddir@/prop/minisat/libminisat.la @builddir@/smt/libsmt.la \
        @builddir@/theory/libtheory.la
-am_libcvc4_noinst_la_OBJECTS =
+am_libcvc4_noinst_la_OBJECTS = empty.lo
 libcvc4_noinst_la_OBJECTS = $(am_libcvc4_noinst_la_OBJECTS)
 DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir)
+depcomp = $(SHELL) $(top_srcdir)/config/depcomp
+am__depfiles_maybe = depfiles
+am__mv = mv -f
+CXXCOMPILE = $(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \
+       $(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS)
+LTCXXCOMPILE = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+       --mode=compile $(CXX) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) \
+       $(AM_CPPFLAGS) $(CPPFLAGS) $(AM_CXXFLAGS) $(CXXFLAGS)
+CXXLD = $(CXX)
+CXXLINK = $(LIBTOOL) --tag=CXX $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
+       --mode=link $(CXXLD) $(AM_CXXFLAGS) $(CXXFLAGS) $(AM_LDFLAGS) \
+       $(LDFLAGS) -o $@
 COMPILE = $(CC) $(DEFS) $(DEFAULT_INCLUDES) $(INCLUDES) $(AM_CPPFLAGS) \
        $(CPPFLAGS) $(AM_CFLAGS) $(CFLAGS)
 LTCOMPILE = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) \
@@ -298,9 +307,14 @@ SUBDIRS = util expr context prop smt theory . parser main
 lib_LTLIBRARIES = libcvc4.la
 noinst_LTLIBRARIES = libcvc4_noinst.la
 libcvc4_la_LDFLAGS = -version-info $(LIBCVC4_VERSION) -release $(LIBCVC4_RELEASE)
+libcvc4_la_LINK = $(CXXLINK)
 libcvc4_la_SOURCES = 
 libcvc4_la_LIBADD = libcvc4_noinst.la
-libcvc4_noinst_la_SOURCES = 
+
+# empty.cpp is a fake file added to "trick" automake into linking us as a
+# C++ library (rather than as a C library, which messes up exception
+# handling support)
+libcvc4_noinst_la_SOURCES = empty.cpp
 libcvc4_noinst_la_LIBADD = \
        @builddir@/util/libutil.la \
        @builddir@/expr/libexpr.la \
@@ -316,6 +330,7 @@ publicheaders = \
 all: all-recursive
 
 .SUFFIXES:
+.SUFFIXES: .cpp .lo .o .obj
 $(srcdir)/Makefile.in:  $(srcdir)/Makefile.am  $(am__configure_deps)
        @for dep in $?; do \
          case '$(am__configure_deps)' in \
@@ -389,7 +404,7 @@ clean-noinstLTLIBRARIES:
 libcvc4.la: $(libcvc4_la_OBJECTS) $(libcvc4_la_DEPENDENCIES) 
        $(libcvc4_la_LINK) -rpath $(libdir) $(libcvc4_la_OBJECTS) $(libcvc4_la_LIBADD) $(LIBS)
 libcvc4_noinst.la: $(libcvc4_noinst_la_OBJECTS) $(libcvc4_noinst_la_DEPENDENCIES) 
-       $(LINK)  $(libcvc4_noinst_la_OBJECTS) $(libcvc4_noinst_la_LIBADD) $(LIBS)
+       $(CXXLINK)  $(libcvc4_noinst_la_OBJECTS) $(libcvc4_noinst_la_LIBADD) $(LIBS)
 
 mostlyclean-compile:
        -rm -f *.$(OBJEXT)
@@ -397,6 +412,29 @@ mostlyclean-compile:
 distclean-compile:
        -rm -f *.tab.c
 
+@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/empty.Plo@am__quote@
+
+.cpp.o:
+@am__fastdepCXX_TRUE@  $(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $<
+@am__fastdepCXX_TRUE@  $(am__mv) $(DEPDIR)/$*.Tpo $(DEPDIR)/$*.Po
+@AMDEP_TRUE@@am__fastdepCXX_FALSE@     source='$<' object='$@' libtool=no @AMDEPBACKSLASH@
+@AMDEP_TRUE@@am__fastdepCXX_FALSE@     DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@
+@am__fastdepCXX_FALSE@ $(CXXCOMPILE) -c -o $@ $<
+
+.cpp.obj:
+@am__fastdepCXX_TRUE@  $(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ `$(CYGPATH_W) '$<'`
+@am__fastdepCXX_TRUE@  $(am__mv) $(DEPDIR)/$*.Tpo $(DEPDIR)/$*.Po
+@AMDEP_TRUE@@am__fastdepCXX_FALSE@     source='$<' object='$@' libtool=no @AMDEPBACKSLASH@
+@AMDEP_TRUE@@am__fastdepCXX_FALSE@     DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@
+@am__fastdepCXX_FALSE@ $(CXXCOMPILE) -c -o $@ `$(CYGPATH_W) '$<'`
+
+.cpp.lo:
+@am__fastdepCXX_TRUE@  $(LTCXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $<
+@am__fastdepCXX_TRUE@  $(am__mv) $(DEPDIR)/$*.Tpo $(DEPDIR)/$*.Plo
+@AMDEP_TRUE@@am__fastdepCXX_FALSE@     source='$<' object='$@' libtool=yes @AMDEPBACKSLASH@
+@AMDEP_TRUE@@am__fastdepCXX_FALSE@     DEPDIR=$(DEPDIR) $(CXXDEPMODE) $(depcomp) @AMDEPBACKSLASH@
+@am__fastdepCXX_FALSE@ $(LTCXXCOMPILE) -c -o $@ $<
+
 mostlyclean-libtool:
        -rm -f *.lo
 
@@ -635,6 +673,7 @@ clean-am: clean-generic clean-libLTLIBRARIES clean-libtool \
        clean-noinstLTLIBRARIES mostlyclean-am
 
 distclean: distclean-recursive
+       -rm -rf ./$(DEPDIR)
        -rm -f Makefile
 distclean-am: clean-am distclean-compile distclean-generic \
        distclean-tags
@@ -680,6 +719,7 @@ install-ps-am:
 installcheck-am:
 
 maintainer-clean: maintainer-clean-recursive
+       -rm -rf ./$(DEPDIR)
        -rm -f Makefile
 maintainer-clean-am: distclean-am maintainer-clean-generic
 
@@ -721,6 +761,9 @@ uninstall-am: uninstall-libLTLIBRARIES
        -D__BUILDING_CVC4LIB \
        -I@srcdir@/include -I@srcdir@
 
+# empty.cpp hack; see above
+empty.cpp:; touch empty.cpp
+
 install-data-local: $(publicheaders)
        $(mkinstalldirs) $(DESTDIR)$(includedir)/cvc4
        @for f in $(publicheaders); do \

diff --git a/src/main/Makefile.am b/src/main/Makefile.am
index f5b76fcfb70e9891b421891b5a8a00bd1c92d498..7c4f2d52d2c4c7ecbc9344b9f64d39ca8e44dab4 100644 (file)
--- a/src/main/Makefile.am
+++ b/src/main/Makefile.am
@@ -1,6 +1,6 @@
 AM_CPPFLAGS = \
        -I@srcdir@/../include -I@srcdir@/..
-AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CXXFLAGS = -Wall
 
 bin_PROGRAMS = cvc4
 
@@ -15,3 +15,5 @@ cvc4_SOURCES = \
 cvc4_LDADD = \
        ../parser/libcvc4parser.la \
        ../libcvc4.la
+
+cvc4_LINK = $(CXXLINK)

diff --git a/src/main/Makefile.in b/src/main/Makefile.in
index 58eeeacdd5b1d33a0d5e5a2181c4de56fe8690b1..8e2c49989a7b420c2bd88bad978475b9ac50856e 100644 (file)
--- a/src/main/Makefile.in
+++ b/src/main/Makefile.in
@@ -222,7 +222,7 @@ top_srcdir = @top_srcdir@
 AM_CPPFLAGS = \
        -I@srcdir@/../include -I@srcdir@/..
 
-AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CXXFLAGS = -Wall
 cvc4_SOURCES = \
        main.cpp \
        getopt.cpp \
@@ -235,6 +235,7 @@ cvc4_LDADD = \
        ../parser/libcvc4parser.la \
        ../libcvc4.la
 
+cvc4_LINK = $(CXXLINK)
 all: all-am
 
 .SUFFIXES:
@@ -314,7 +315,7 @@ clean-binPROGRAMS:
        rm -f $$list
 cvc4$(EXEEXT): $(cvc4_OBJECTS) $(cvc4_DEPENDENCIES) 
        @rm -f cvc4$(EXEEXT)
-       $(CXXLINK) $(cvc4_OBJECTS) $(cvc4_LDADD) $(LIBS)
+       $(cvc4_LINK) $(cvc4_OBJECTS) $(cvc4_LDADD) $(LIBS)
 
 mostlyclean-compile:
        -rm -f *.$(OBJEXT)

diff --git a/src/main/main.cpp b/src/main/main.cpp
index ba71b043f348278a470ec3832bb543a34aff0291..6f32e474b4240039750d55933ddd626c62679c48 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -28,6 +28,7 @@
 #include "expr/expr_manager.h"
 #include "smt/smt_engine.h"
 #include "util/command.h"
+#include "util/Assert.h"
 #include "util/output.h"
 #include "util/options.h"
 
@@ -55,7 +56,7 @@ int main(int argc, char *argv[]) {
 
     // We only accept one input file
     if(argc > firstArgIndex + 1) {
-      throw new Exception("Too many input files specified.");
+      throw Exception("Too many input files specified.");
     }
 
     // Create the expression manager
@@ -144,8 +145,10 @@ int main(int argc, char *argv[]) {
     // Remove the parser
     delete parser;
 
-    // Delete handle to input file
-    delete file;
+    if(! inputFromStdin) {
+      // Delete handle to input file
+      delete file;
+    }
   } catch(OptionException& e) {
     if(options.smtcomp_mode) {
       cout << "unknown" << endl;
@@ -153,7 +156,7 @@ int main(int argc, char *argv[]) {
     cerr << "CVC4 Error:" << endl << e << endl;
     printf(usage, options.binary_name.c_str());
     abort();
-  } catch(CVC4::Exception& e) {
+  } catch(Exception& e) {
     if(options.smtcomp_mode) {
       cout << "unknown" << endl;
     }

diff --git a/src/main/util.cpp b/src/main/util.cpp
index 9bb96d85381c12c37eff06bf91327ab74ff3412e..0b33b145dfc80b2455281cb7b6d8bf23127f0584 100644 (file)
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -46,14 +46,14 @@ void cvc4_init() throw() {
   act1.sa_flags = SA_SIGINFO;
   sigemptyset(&act1.sa_mask);
   if(sigaction(SIGINT, &act1, NULL))
-    throw new Exception(string("sigaction(SIGINT) failure: ") + strerror(errno));
+    throw Exception(string("sigaction(SIGINT) failure: ") + strerror(errno));
 
   struct sigaction act2;
   act2.sa_sigaction = segv_handler;
   act2.sa_flags = SA_SIGINFO;
   sigemptyset(&act2.sa_mask);
   if(sigaction(SIGSEGV, &act2, NULL))
-    throw new Exception(string("sigaction(SIGSEGV) failure: ") + strerror(errno));
+    throw Exception(string("sigaction(SIGSEGV) failure: ") + strerror(errno));
 }
 
 }/* CVC4::main namespace */

diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index 86c088246edbd15b26cf9030d5f0f91c2f2734d5..4fcaed14d4f1d5cb2043660fb131f3f7c55ae9b6 100644 (file)
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -27,6 +27,7 @@ noinst_LTLIBRARIES = libcvc4parser_noinst.la
 
 libcvc4parser_la_LDFLAGS = $(ANTLR_LDFLAGS)
 libcvc4parser_la_LIBADD = libcvc4parser_noinst.la
+libcvc4parser_la_LINK = $(CXXLINK)
 
 libcvc4parser_noinst_la_LDFLAGS = $(ANTLR_LDFLAGS)
 libcvc4parser_noinst_la_LIBADD = \

diff --git a/src/parser/Makefile.in b/src/parser/Makefile.in
index 3b703efa01077ab94e6640aa2e717eff6d141486..31ae05da56abc71887e11019d06e869cfa1871f8 100644 (file)
--- a/src/parser/Makefile.in
+++ b/src/parser/Makefile.in
@@ -76,9 +76,6 @@ LTLIBRARIES = $(nobase_lib_LTLIBRARIES) $(noinst_LTLIBRARIES)
 libcvc4parser_la_DEPENDENCIES = libcvc4parser_noinst.la
 am_libcvc4parser_la_OBJECTS =
 libcvc4parser_la_OBJECTS = $(am_libcvc4parser_la_OBJECTS)
-libcvc4parser_la_LINK = $(LIBTOOL) --tag=CC $(AM_LIBTOOLFLAGS) \
-       $(LIBTOOLFLAGS) --mode=link $(CCLD) $(AM_CFLAGS) $(CFLAGS) \
-       $(libcvc4parser_la_LDFLAGS) $(LDFLAGS) -o $@
 libcvc4parser_noinst_la_DEPENDENCIES = @builddir@/smt/libparsersmt.la \
        @builddir@/cvc/libparsercvc.la
 am_libcvc4parser_noinst_la_OBJECTS = parser.lo antlr_parser.lo
@@ -318,6 +315,7 @@ nobase_lib_LTLIBRARIES = libcvc4parser.la
 noinst_LTLIBRARIES = libcvc4parser_noinst.la
 libcvc4parser_la_LDFLAGS = $(ANTLR_LDFLAGS)
 libcvc4parser_la_LIBADD = libcvc4parser_noinst.la
+libcvc4parser_la_LINK = $(CXXLINK)
 libcvc4parser_noinst_la_LDFLAGS = $(ANTLR_LDFLAGS)
 libcvc4parser_noinst_la_LIBADD = \
        @builddir@/smt/libparsersmt.la \

diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 61eef32d56223907c0395dd673687bdc340f2cc9..f05a74bcf9b2258f1ab132da0bf68dc10cd55de1 100644 (file)
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -7,7 +7,7 @@ UNIT_TESTS = \
 
 # things that aren't tests but that tests rely on and need to
 # go into the distribution
-TEST_DEPENDENCIES =
+TEST_DEPS =
 
 if HAVE_CXXTESTGEN
 
@@ -21,10 +21,10 @@ AM_CXXFLAGS_WHITE = -fno-access-control
 AM_CXXFLAGS_BLACK =
 AM_CXXFLAGS_PUBLIC =
 AM_LDFLAGS_WHITE = \
-       @abs_top_builddir@/src/parser/libcvc4parser_noinst.la \ 
+       @abs_top_builddir@/src/parser/libcvc4parser_noinst.la \
        @abs_top_builddir@/src/libcvc4_noinst.la
 AM_LDFLAGS_BLACK = \
-       @abs_top_builddir@/src/parser/libcvc4parser_noinst.la \ 
+       @abs_top_builddir@/src/parser/libcvc4parser_noinst.la \
        @abs_top_builddir@/src/libcvc4_noinst.la
 AM_LDFLAGS_PUBLIC = \
        @abs_top_builddir@/src/libcvc4.la
@@ -33,7 +33,7 @@ TESTS = $(UNIT_TESTS)
 
 EXTRA_DIST = \
        no_cxxtest \
-       $(TEST_DEPENDENCIES)
+       $(TEST_DEPS)
 
 # without these here, LTCXXCOMPILE, CXXLINK, etc., aren't set :-(
 noinst_LTLIBRARIES = libdummy.la
@@ -62,6 +62,6 @@ TESTS = no_cxxtest
 
 EXTRA_DIST = \
        $(UNIT_TESTS) \
-       $(TEST_DEPENDENCIES)
+       $(TEST_DEPS)
 
 endif

diff --git a/test/unit/Makefile.in b/test/unit/Makefile.in
index 6e518d52759e59c169cb8ee7ac1e9b4a35970550..a3bb01929723ba859dcf48a0e54e17bbe9f6fd57 100644 (file)
--- a/test/unit/Makefile.in
+++ b/test/unit/Makefile.in
@@ -224,7 +224,7 @@ UNIT_TESTS = \
 
 # things that aren't tests but that tests rely on and need to
 # go into the distribution
-TEST_DEPENDENCIES = 
+TEST_DEPS = 
 @HAVE_CXXTESTGEN_TRUE@AM_CPPFLAGS = \
 @HAVE_CXXTESTGEN_TRUE@ -I. "-I@CXXTEST@" "-I@top_srcdir@/src/include" "-I@top_srcdir@/src" \
 @HAVE_CXXTESTGEN_TRUE@ $(TEST_CPPFLAGS)
@@ -251,11 +251,11 @@ TEST_DEPENDENCIES =
 @HAVE_CXXTESTGEN_TRUE@TESTS = $(UNIT_TESTS)
 @HAVE_CXXTESTGEN_FALSE@EXTRA_DIST = \
 @HAVE_CXXTESTGEN_FALSE@        $(UNIT_TESTS) \
-@HAVE_CXXTESTGEN_FALSE@        $(TEST_DEPENDENCIES)
+@HAVE_CXXTESTGEN_FALSE@        $(TEST_DEPS)
 
 @HAVE_CXXTESTGEN_TRUE@EXTRA_DIST = \
 @HAVE_CXXTESTGEN_TRUE@ no_cxxtest \
-@HAVE_CXXTESTGEN_TRUE@ $(TEST_DEPENDENCIES)
+@HAVE_CXXTESTGEN_TRUE@ $(TEST_DEPS)
 
 
 # without these here, LTCXXCOMPILE, CXXLINK, etc., aren't set :-(

diff --git a/test/unit/parser/smt/smt_parser_black.h b/test/unit/parser/smt/smt_parser_black.h
index 3b4b812395d1b01d0b33b69663624a3805f9f2b6..7ec46b16c8e2a3d1cfc58604baabdd10459df88e 100644 (file)
--- a/test/unit/parser/smt/smt_parser_black.h
+++ b/test/unit/parser/smt/smt_parser_black.h
@@ -1,4 +1,17 @@
-/* Black box testing of smt4::parser:SmtParser. */
+/*********************                                           -*- C++ -*-  */
+/** smt_parser_black.h
+ ** Original author: cconway
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Black box testing of CVC4::parser::SmtParser.
+ **/
 
 #include <cxxtest/TestSuite.h>
 //#include <string>