summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Makefile.am9
-rw-r--r--src/Makefile.in55
-rw-r--r--src/main/Makefile.am4
-rw-r--r--src/main/Makefile.in5
-rw-r--r--src/main/main.cpp11
-rw-r--r--src/main/util.cpp4
-rw-r--r--src/parser/Makefile.am1
-rw-r--r--src/parser/Makefile.in4
-rw-r--r--test/unit/Makefile.am10
-rw-r--r--test/unit/Makefile.in6
-rw-r--r--test/unit/parser/smt/smt_parser_black.h15
11 files changed, 96 insertions, 28 deletions
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 <cxxtest/TestSuite.h>
//#include <string>
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback