From 38a13fe227e6b59a49509d4b5ae6618b4c14937a Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 27 Jun 2013 15:35:24 -0400 Subject: [PATCH] Remove output.h from public space, to avoid clashes with symbols defined in users' space. Specifically, output.h was moved to CVC4's "private-library" rules, which means that it's not installed on users' machines, and public headers should not include it. Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list. --- src/compat/cvc3_compat.cpp | 1 + src/include/cvc4_private_library.h | 2 +- src/main/interactive_shell.cpp | 1 + src/parser/antlr_input.h | 12 +++++++++++- src/parser/antlr_line_buffered_input.cpp | 9 +++++++++ src/util/datatype.h | 1 - src/util/dump.h | 1 - src/util/output.h | 2 +- test/unit/expr/expr_public.h | 2 +- test/unit/expr/type_cardinality_public.h | 2 +- 10 files changed, 26 insertions(+), 7 deletions(-) diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 601c251d9..1ac277667 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -25,6 +25,7 @@ #include "util/hash.h" #include "util/subrange_bound.h" #include "util/predicate.h" +#include "util/output.h" #include "parser/parser.h" #include "parser/parser_builder.h" diff --git a/src/include/cvc4_private_library.h b/src/include/cvc4_private_library.h index b04160a81..f7fd1b607 100644 --- a/src/include/cvc4_private_library.h +++ b/src/include/cvc4_private_library.h @@ -19,7 +19,7 @@ #ifndef __CVC4_PRIVATE_LIBRARY_H #define __CVC4_PRIVATE_LIBRARY_H -#if ! (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST) || defined(__BUILDING_CVC4PARSERLIB) || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST) || defined(__BUILDING_CVC4DRIVER)) +#if ! (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST) || defined(__BUILDING_CVC4PARSERLIB) || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST) || defined(__BUILDING_CVC4COMPATLIB) || defined(__BUILDING_CVC4DRIVER)) # warning A "private library" CVC4 header was included when not building the library, driver, or private unit test code. #endif /* ! (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST || __BUILDING_CVC4PARSERLIB || __BUILDING_CVC4PARSERLIB_UNIT_TEST || __BUILDING_CVC4DRIVER) */ diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 5c9f8af21..a8099ca30 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -33,6 +33,7 @@ #include "parser/parser_builder.h" #include "options/options.h" #include "util/language.h" +#include "util/output.h" #include #include diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index 3b7d53be8..8763e8451 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -14,12 +14,21 @@ ** Base for ANTLR parser classes. **/ +#include + +// ANTLR3 headers define these in our space :( +// undef them so that we don't get multiple-definition warnings +#undef PACKAGE_BUGREPORT +#undef PACKAGE_NAME +#undef PACKAGE_STRING +#undef PACKAGE_TARNAME +#undef PACKAGE_VERSION + #include "cvc4parser_private.h" #ifndef __CVC4__PARSER__ANTLR_INPUT_H #define __CVC4__PARSER__ANTLR_INPUT_H -#include #include #include #include @@ -34,6 +43,7 @@ #include "util/bitvector.h" #include "util/integer.h" #include "util/rational.h" +#include "util/output.h" namespace CVC4 { diff --git a/src/parser/antlr_line_buffered_input.cpp b/src/parser/antlr_line_buffered_input.cpp index c2f73d988..a59fb3531 100644 --- a/src/parser/antlr_line_buffered_input.cpp +++ b/src/parser/antlr_line_buffered_input.cpp @@ -16,6 +16,15 @@ **/ #include + +// ANTLR3 headers define these in our space :( +// undef them so that we don't get multiple-definition warnings +#undef PACKAGE_BUGREPORT +#undef PACKAGE_NAME +#undef PACKAGE_STRING +#undef PACKAGE_TARNAME +#undef PACKAGE_VERSION + #include #include #include diff --git a/src/util/datatype.h b/src/util/datatype.h index 3da441f1f..c46c10c97 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -33,7 +33,6 @@ namespace CVC4 { #include "expr/expr.h" #include "expr/type.h" -#include "util/output.h" #include "util/hash.h" #include "util/exception.h" diff --git a/src/util/dump.h b/src/util/dump.h index 2ef6010e3..0bde68d76 100644 --- a/src/util/dump.h +++ b/src/util/dump.h @@ -19,7 +19,6 @@ #ifndef __CVC4__DUMP_H #define __CVC4__DUMP_H -#include "util/output.h" #include "expr/command.h" namespace CVC4 { diff --git a/src/util/output.h b/src/util/output.h index 263d5a144..7394f24ab 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -14,7 +14,7 @@ ** Output utility classes and functions. **/ -#include "cvc4_public.h" +#include "cvc4_private_library.h" #ifndef __CVC4__OUTPUT_H #define __CVC4__OUTPUT_H diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h index c66b5cb1f..7f6385d36 100644 --- a/test/unit/expr/expr_public.h +++ b/test/unit/expr/expr_public.h @@ -342,7 +342,7 @@ public: void testIsConst() { /* bool isConst() const; */ - Debug.on("isConst"); + //Debug.on("isConst"); TS_ASSERT(!a_bool->isConst()); TS_ASSERT(!b_bool->isConst()); diff --git a/test/unit/expr/type_cardinality_public.h b/test/unit/expr/type_cardinality_public.h index 2441b7b0d..3c2609e3e 100644 --- a/test/unit/expr/type_cardinality_public.h +++ b/test/unit/expr/type_cardinality_public.h @@ -200,7 +200,7 @@ public: } void testBitvectors() { - Debug.on("bvcard"); + //Debug.on("bvcard"); TS_ASSERT( d_em->mkBitVectorType(0).getCardinality().compare(0) == Cardinality::EQUAL ); Cardinality lastCard = 0; for(unsigned i = 1; i <= 65; ++i) { -- 2.30.2