From d8967f559330d19f342e7313f4e45a10c1bec6ba Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 11 Feb 2018 15:45:55 +0000 Subject: [PATCH] moving language.h and language_file.h to langapi folder The languaget API has become excessively cluttered, and will be phased out. In preparation, the files are moved to the langapi folder. --- src/ansi-c/ansi_c_language.h | 3 ++- src/cbmc/cbmc_parse_options.cpp | 3 ++- src/cbmc/cbmc_parse_options.h | 3 ++- src/clobber/clobber_parse_options.cpp | 1 - src/cpp/cpp_language.h | 3 ++- src/goto-analyzer/goto_analyzer_parse_options.cpp | 2 +- src/goto-analyzer/goto_analyzer_parse_options.h | 3 ++- src/goto-diff/goto_diff_parse_options.cpp | 3 ++- src/goto-instrument/dump_c_class.h | 4 ++-- src/goto-instrument/splice_call.cpp | 6 +++++- src/goto-programs/initialize_goto_model.cpp | 2 +- src/goto-programs/lazy_goto_functions_map.h | 4 +++- src/goto-programs/lazy_goto_model.cpp | 3 ++- src/goto-programs/lazy_goto_model.h | 2 +- src/goto-programs/rebuild_goto_start_function.cpp | 4 +++- src/goto-programs/show_symbol_table.cpp | 2 +- src/java_bytecode/java_bytecode_language.h | 3 ++- src/jbmc/jbmc_parse_options.cpp | 3 ++- src/jbmc/jbmc_parse_options.h | 3 ++- src/jsil/jsil_language.h | 3 ++- src/langapi/Makefile | 2 ++ src/{util => langapi}/language.cpp | 2 +- src/{util => langapi}/language.h | 9 +++++---- src/{util => langapi}/language_file.cpp | 0 src/{util => langapi}/language_file.h | 9 +++++---- src/langapi/language_ui.cpp | 2 +- src/langapi/language_ui.h | 3 ++- src/langapi/language_util.cpp | 2 +- src/langapi/mode.cpp | 2 +- src/util/Makefile | 2 -- src/util/json_expr.cpp | 2 +- .../convert_abstract_class.cpp | 3 ++- unit/testing-utils/load_java_class.cpp | 1 - unit/testing-utils/load_java_class.h | 4 +++- 34 files changed, 63 insertions(+), 40 deletions(-) rename src/{util => langapi}/language.cpp (99%) rename src/{util => langapi}/language.h (97%) rename src/{util => langapi}/language_file.cpp (100%) rename src/{util => langapi}/language_file.h (96%) diff --git a/src/ansi-c/ansi_c_language.h b/src/ansi-c/ansi_c_language.h index 78119020c97..949f266d2c9 100644 --- a/src/ansi-c/ansi_c_language.h +++ b/src/ansi-c/ansi_c_language.h @@ -14,9 +14,10 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include +#include + #include "ansi_c_parse_tree.h" class ansi_c_languaget:public languaget diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 5aec984a857..1b83f244e01 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -18,12 +18,13 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include #include +#include + #include #include diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 4de4c4a1fcf..60e112da456 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -14,7 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include + +#include #include diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp index b59cd44fae3..3f36a615272 100644 --- a/src/clobber/clobber_parse_options.cpp +++ b/src/clobber/clobber_parse_options.cpp @@ -17,7 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include diff --git a/src/cpp/cpp_language.h b/src/cpp/cpp_language.h index fcfbaa38299..613adcbac0f 100644 --- a/src/cpp/cpp_language.h +++ b/src/cpp/cpp_language.h @@ -16,9 +16,10 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include -#include #include // unique_ptr +#include + #include "cpp_parse_tree.h" class cpp_languaget:public languaget diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 9b92bf94cff..fc37947e56a 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -46,8 +46,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include -#include #include #include #include diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index 98181e385d7..dc5c8cdf80d 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -103,7 +103,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include + +#include #include #include diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 26809476b35..2f5701dde02 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -18,10 +18,11 @@ Author: Peter Schrammel #include #include -#include #include #include +#include + #include #include #include diff --git a/src/goto-instrument/dump_c_class.h b/src/goto-instrument/dump_c_class.h index 904861fa5bd..40d32b9a64e 100644 --- a/src/goto-instrument/dump_c_class.h +++ b/src/goto-instrument/dump_c_class.h @@ -16,9 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include // unique_ptr -#include - +#include #include + #include class dump_ct diff --git a/src/goto-instrument/splice_call.cpp b/src/goto-instrument/splice_call.cpp index f8e13872d98..1e45865e352 100644 --- a/src/goto-instrument/splice_call.cpp +++ b/src/goto-instrument/splice_call.cpp @@ -14,11 +14,15 @@ Date: July 2017 // useful for context/ environment setting in arbitrary nodes #include "splice_call.h" + #include #include #include -#include + +#include + #include + #include // split the argument in caller/ callee two-position vector diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp index 13953d721b4..564a0a1eaad 100644 --- a/src/goto-programs/initialize_goto_model.cpp +++ b/src/goto-programs/initialize_goto_model.cpp @@ -14,12 +14,12 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include #include +#include #include diff --git a/src/goto-programs/lazy_goto_functions_map.h b/src/goto-programs/lazy_goto_functions_map.h index c52243e0580..8f948515c56 100644 --- a/src/goto-programs/lazy_goto_functions_map.h +++ b/src/goto-programs/lazy_goto_functions_map.h @@ -7,10 +7,12 @@ #define CPROVER_GOTO_PROGRAMS_LAZY_GOTO_FUNCTIONS_MAP_H #include + #include "goto_functions.h" #include "goto_convert_functions.h" + #include -#include +#include #include /// Provides a wrapper for a map of lazily loaded goto_functiont. diff --git a/src/goto-programs/lazy_goto_model.cpp b/src/goto-programs/lazy_goto_model.cpp index cde0250f12e..4c0ee749554 100644 --- a/src/goto-programs/lazy_goto_model.cpp +++ b/src/goto-programs/lazy_goto_model.cpp @@ -12,9 +12,10 @@ #include #include #include -#include #include +#include + #include //! @cond Doxygen_suppress_Lambda_in_initializer_list diff --git a/src/goto-programs/lazy_goto_model.h b/src/goto-programs/lazy_goto_model.h index 362df30c0fb..4419d994846 100644 --- a/src/goto-programs/lazy_goto_model.h +++ b/src/goto-programs/lazy_goto_model.h @@ -6,7 +6,7 @@ #ifndef CPROVER_GOTO_PROGRAMS_LAZY_GOTO_MODEL_H #define CPROVER_GOTO_PROGRAMS_LAZY_GOTO_MODEL_H -#include +#include #include "goto_model.h" #include "lazy_goto_functions_map.h" diff --git a/src/goto-programs/rebuild_goto_start_function.cpp b/src/goto-programs/rebuild_goto_start_function.cpp index 8621ff4a44c..e785dd95343 100644 --- a/src/goto-programs/rebuild_goto_start_function.cpp +++ b/src/goto-programs/rebuild_goto_start_function.cpp @@ -8,12 +8,14 @@ #include "rebuild_goto_start_function.h" -#include #include #include #include #include + #include +#include + #include /// To rebuild the _start function in the event the program was compiled into diff --git a/src/goto-programs/show_symbol_table.cpp b/src/goto-programs/show_symbol_table.cpp index b4230f9086b..f65728df11b 100644 --- a/src/goto-programs/show_symbol_table.cpp +++ b/src/goto-programs/show_symbol_table.cpp @@ -14,7 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include #include "goto_model.h" diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h index d267cb9b218..e75fb39dc31 100644 --- a/src/java_bytecode/java_bytecode_language.h +++ b/src/java_bytecode/java_bytecode_language.h @@ -12,10 +12,11 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include #include +#include + #include "ci_lazy_methods.h" #include "ci_lazy_methods_needed.h" #include "java_class_loader.h" diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index fb5efc6634d..2e5270a63fc 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -18,11 +18,12 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include +#include + #include #include diff --git a/src/jbmc/jbmc_parse_options.h b/src/jbmc/jbmc_parse_options.h index 327e9aa7ca2..aa221424d9c 100644 --- a/src/jbmc/jbmc_parse_options.h +++ b/src/jbmc/jbmc_parse_options.h @@ -14,7 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include + +#include #include diff --git a/src/jsil/jsil_language.h b/src/jsil/jsil_language.h index 91df43e6266..8b902b86ded 100644 --- a/src/jsil/jsil_language.h +++ b/src/jsil/jsil_language.h @@ -14,9 +14,10 @@ Author: Michael Tautschnig, tautschn@amazon.com #include -#include #include +#include + #include "jsil_parse_tree.h" class jsil_languaget:public languaget diff --git a/src/langapi/Makefile b/src/langapi/Makefile index 5d650c55c8b..ea85a9213b8 100644 --- a/src/langapi/Makefile +++ b/src/langapi/Makefile @@ -1,5 +1,7 @@ SRC = language_ui.cpp \ language_util.cpp \ + language_file.cpp \ + language.cpp \ mode.cpp \ # Empty last line INCLUDES= -I .. diff --git a/src/util/language.cpp b/src/langapi/language.cpp similarity index 99% rename from src/util/language.cpp rename to src/langapi/language.cpp index 60ea1262646..443062dce08 100644 --- a/src/util/language.cpp +++ b/src/langapi/language.cpp @@ -11,7 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "language.h" -#include "expr.h" +#include #include #include #include diff --git a/src/util/language.h b/src/langapi/language.h similarity index 97% rename from src/util/language.h rename to src/langapi/language.h index fe23e5b3186..06d145965f0 100644 --- a/src/util/language.h +++ b/src/langapi/language.h @@ -9,18 +9,19 @@ Author: Daniel Kroening, kroening@kroening.com /// \file /// Abstract interface to support a programming language -#ifndef CPROVER_UTIL_LANGUAGE_H -#define CPROVER_UTIL_LANGUAGE_H +#ifndef CPROVER_LANGAPI_LANGUAGE_H +#define CPROVER_LANGAPI_LANGUAGE_H #include #include #include #include // unique_ptr + #include #include -#include +#include -#include "message.h" +#include typedef std::unordered_set id_sett; diff --git a/src/util/language_file.cpp b/src/langapi/language_file.cpp similarity index 100% rename from src/util/language_file.cpp rename to src/langapi/language_file.cpp diff --git a/src/util/language_file.h b/src/langapi/language_file.h similarity index 96% rename from src/util/language_file.h rename to src/langapi/language_file.h index fb71b06a336..046a11a5d55 100644 --- a/src/util/language_file.h +++ b/src/langapi/language_file.h @@ -7,8 +7,8 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#ifndef CPROVER_UTIL_LANGUAGE_FILE_H -#define CPROVER_UTIL_LANGUAGE_FILE_H +#ifndef CPROVER_LANGAPI_LANGUAGE_FILE_H +#define CPROVER_LANGAPI_LANGUAGE_FILE_H #include #include @@ -16,8 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include // unique_ptr -#include "message.h" -#include "symbol_table.h" +#include +#include + #include "language.h" class language_filet; diff --git a/src/langapi/language_ui.cpp b/src/langapi/language_ui.cpp index 560fd43bb89..a157cc68359 100644 --- a/src/langapi/language_ui.cpp +++ b/src/langapi/language_ui.cpp @@ -13,11 +13,11 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include -#include #include #include #include +#include "language.h" #include "mode.h" /// Constructor diff --git a/src/langapi/language_ui.h b/src/langapi/language_ui.h index 76fe7f2445c..44760c06648 100644 --- a/src/langapi/language_ui.h +++ b/src/langapi/language_ui.h @@ -11,10 +11,11 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #define CPROVER_LANGAPI_LANGUAGE_UI_H #include -#include #include #include +#include "language_file.h" + class cmdlinet; class language_uit:public messaget diff --git a/src/langapi/language_util.cpp b/src/langapi/language_util.cpp index 06398eea3da..7a2e691af38 100644 --- a/src/langapi/language_util.cpp +++ b/src/langapi/language_util.cpp @@ -12,9 +12,9 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include -#include #include +#include "language.h" #include "mode.h" static std::unique_ptr get_language( diff --git a/src/langapi/mode.cpp b/src/langapi/mode.cpp index 8d1d9128010..dd12882c544 100644 --- a/src/langapi/mode.cpp +++ b/src/langapi/mode.cpp @@ -16,7 +16,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #endif -#include +#include "language.h" struct language_entryt { diff --git a/src/util/Makefile b/src/util/Makefile index 0b1f8aa67a8..338f081ff3b 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -35,8 +35,6 @@ SRC = arith_tools.cpp \ json.cpp \ json_expr.cpp \ json_irep.cpp \ - language.cpp \ - language_file.cpp \ lispexpr.cpp \ lispirep.cpp \ memory_info.cpp \ diff --git a/src/util/json_expr.cpp b/src/util/json_expr.cpp index b2aa92bb199..aa8b63a0dc7 100644 --- a/src/util/json_expr.cpp +++ b/src/util/json_expr.cpp @@ -20,10 +20,10 @@ Author: Peter Schrammel #include "std_expr.h" #include "config.h" #include "identifier.h" -#include "language.h" #include "invariant.h" #include +#include #include diff --git a/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp b/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp index 406291025ad..bab86c5a011 100644 --- a/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp +++ b/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp @@ -12,9 +12,10 @@ #include #include -#include #include + #include + #include SCENARIO("java_bytecode_convert_abstract_class", diff --git a/unit/testing-utils/load_java_class.cpp b/unit/testing-utils/load_java_class.cpp index 0f112b0d2e4..5440bd9d79b 100644 --- a/unit/testing-utils/load_java_class.cpp +++ b/unit/testing-utils/load_java_class.cpp @@ -11,7 +11,6 @@ #include #include -#include #include #include diff --git a/unit/testing-utils/load_java_class.h b/unit/testing-utils/load_java_class.h index dc66a171511..c9fd887d2c5 100644 --- a/unit/testing-utils/load_java_class.h +++ b/unit/testing-utils/load_java_class.h @@ -14,9 +14,11 @@ #define CPROVER_TESTING_UTILS_LOAD_JAVA_CLASS_H #include -#include + #include +#include + symbol_tablet load_java_class( const std::string &java_class_name, const std::string &class_path,