diff options
Diffstat (limited to 'src/parser/antlr_undefines.h')
| -rw-r--r-- | src/parser/antlr_undefines.h | 69 |
1 files changed, 0 insertions, 69 deletions
diff --git a/src/parser/antlr_undefines.h b/src/parser/antlr_undefines.h deleted file mode 100644 index 20df6dbc7..000000000 --- a/src/parser/antlr_undefines.h +++ /dev/null @@ -1,69 +0,0 @@ -/********************* */ -/*! \file antlr_undefines.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Every usage undefines standard autotools macro names. - ** - ** This header is very sensitive and it should be understood *in full* before - ** it is used or *moved* in position relative to other headers. - ** - ** Including this header runs #undef on the following identifiers: - ** - PACKAGE_BUGREPORT, - ** - PACKAGE_NAME - ** - PACKAGE_STRING - ** - PACKAGE_TARNAME - ** - PACKAGE_VERSION - ** - ** This is to solves a problem caused by antlr and cvc4 both defining these - ** symbols. This has to do with both packages using autotools in a slightly - ** dicey way. This was reported by us a long time ago, but most versions - ** of libantlr are quite old (3.2). - ** http://www.antlr3.org/pipermail/antlr-interest/2010-March/037859.html - ** - ** The source of both of these two definitions are given below. - ** - ** From antlr, the autogenerated antlr lexers and parsers include antlr3.h. - ** The chain of inclusions is: - ** Lang{Lexer,Parser}.h -> <antlr3.h> -> <antlr3config.h> -> <antlr3defs.h> - ** - ** where Lang is in {Smt1,Smt2,Tptp,Cvc}. - ** - ** From CVC4, the parsers use Debug("...") and other features from - ** "base/output.h". This is a cvc4_private_library.h header file. This means - ** the files is usable while building the driver and parsers, but is otherwise - ** conceptually the same as a cvc4_private.h header. (If that sounds sketchy, - ** it is sure is! [See src/DESIGN.txt for more details].) - ** The include chain is then - ** "base/output.h" -> "cvc4_private_library.h" -> "cvc4_private.h" -> - ** "cvc4autoconfig.h". - ** The file cvc4autoconfig.h is autogenerated by autotools and can be found in - ** builds/<arch>/<target>/cvc4autoconfig.h - ** - ** Thus a working solution is to include this header immediately after all - ** locations of #include <antlr3.h>. This includes all autogenerated files. - ** This potentially has to be repeated so this header should not be guarded. - ** - ** To ensure that we do not remove cvc4's versions and use antlr's by mistake - ** #include <antlr3.h> needs to proceed any other includes like - ** #include "cvc4parser_private.h". - ** - ** It is worth noting that future version of antlr can both not define these - ** macros and may generate different code. This is at best a stop gap - ** solution. - ** - ** Every location this header is included needs to be documented. - ** When in doubt do not move this header! - **/ - -#undef PACKAGE_BUGREPORT -#undef PACKAGE_NAME -#undef PACKAGE_STRING -#undef PACKAGE_TARNAME -#undef PACKAGE_VERSION |