From: Morgan Deters Date: Thu, 17 Dec 2009 22:11:37 +0000 (+0000) Subject: more build system fix-ups X-Git-Tag: cvc5-1.0.0~9355 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=093492af43fae12d7f1d4607e63b1da686044ea6;p=cvc5.git more build system fix-ups --- diff --git a/src/Makefile.am b/src/Makefile.am index 110ab9855..97a2ecead 100644 --- 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 c650c1503..9099b92be 100644 --- 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 f5b76fcfb..7c4f2d52d 100644 --- 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 58eeeacdd..8e2c49989 100644 --- 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 ba71b043f..6f32e474b 100644 --- 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 9bb96d853..0b33b145d 100644 --- 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 86c088246..4fcaed14d 100644 --- 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 3b703efa0..31ae05da5 100644 --- 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 61eef32d5..f05a74bcf 100644 --- 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 6e518d527..a3bb01929 100644 --- 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 3b4b81239..7ec46b16c 100644 --- 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 //#include