diff --git a/jbmc/src/jbmc/Makefile b/jbmc/src/jbmc/Makefile index 1344b1beb4a..f87d8d3662d 100644 --- a/jbmc/src/jbmc/Makefile +++ b/jbmc/src/jbmc/Makefile @@ -32,7 +32,6 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \ ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_mcdc$(OBJEXT) \ ../$(CPROVER_DIR)/src/goto-instrument/cover_instrument_other$(OBJEXT) \ ../$(CPROVER_DIR)/src/goto-instrument/cover_util$(OBJEXT) \ - ../$(CPROVER_DIR)/src/goto-instrument/unwindset$(OBJEXT) \ ../$(CPROVER_DIR)/src/analyses/analyses$(LIBEXT) \ ../$(CPROVER_DIR)/src/langapi/langapi$(LIBEXT) \ ../$(CPROVER_DIR)/src/xmllang/xmllang$(LIBEXT) \ diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index bbe89ee617c..bc16c2ca851 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -116,7 +116,6 @@ CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \ $(CPROVER_DIR)/src/goto-instrument/reachability_slicer$(OBJEXT) \ $(CPROVER_DIR)/src/goto-instrument/nondet_static$(OBJEXT) \ $(CPROVER_DIR)/src/goto-instrument/full_slicer$(OBJEXT) \ - $(CPROVER_DIR)/src/goto-instrument/unwindset$(OBJEXT) \ $(CPROVER_DIR)/src/pointer-analysis/pointer-analysis$(LIBEXT) \ $(CPROVER_DIR)/src/langapi/langapi$(LIBEXT) \ $(CPROVER_DIR)/src/xmllang/xmllang$(LIBEXT) \ diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index d78b9221461..cc5be488a55 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -36,7 +36,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../goto-instrument/reachability_slicer$(OBJEXT) \ ../goto-instrument/nondet_static$(OBJEXT) \ ../goto-instrument/full_slicer$(OBJEXT) \ - ../goto-instrument/unwindset$(OBJEXT) \ ../analyses/analyses$(LIBEXT) \ ../langapi/langapi$(LIBEXT) \ ../xmllang/xmllang$(LIBEXT) \ diff --git a/src/goto-checker/CMakeLists.txt b/src/goto-checker/CMakeLists.txt index 9b9f9698bac..7f75ff54011 100644 --- a/src/goto-checker/CMakeLists.txt +++ b/src/goto-checker/CMakeLists.txt @@ -3,4 +3,4 @@ add_library(goto-checker ${sources}) generic_includes(goto-checker) -target_link_libraries(goto-checker goto-programs goto-symex solvers util xml goto-instrument-lib) +target_link_libraries(goto-checker goto-programs goto-symex solvers util xml) diff --git a/src/goto-checker/bmc_util.h b/src/goto-checker/bmc_util.h index 92e0e3a82de..292d9c14ddc 100644 --- a/src/goto-checker/bmc_util.h +++ b/src/goto-checker/bmc_util.h @@ -12,7 +12,8 @@ Author: Daniel Kroening, Peter Schrammel #ifndef CPROVER_GOTO_CHECKER_BMC_UTIL_H #define CPROVER_GOTO_CHECKER_BMC_UTIL_H -#include +#include + #include #include "incremental_goto_checker.h" diff --git a/src/goto-checker/module_dependencies.txt b/src/goto-checker/module_dependencies.txt index fbac8e83b49..07af9cc962d 100644 --- a/src/goto-checker/module_dependencies.txt +++ b/src/goto-checker/module_dependencies.txt @@ -1,7 +1,6 @@ assembler cbmc # symex_bmc will be moved next goto-checker -goto-instrument goto-programs goto-symex langapi diff --git a/src/goto-checker/multi_path_symex_only_checker.h b/src/goto-checker/multi_path_symex_only_checker.h index 0bd396eb4c1..b8e8b3ab116 100644 --- a/src/goto-checker/multi_path_symex_only_checker.h +++ b/src/goto-checker/multi_path_symex_only_checker.h @@ -12,12 +12,11 @@ Author: Daniel Kroening, Peter Schrammel #ifndef CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_ONLY_CHECKER_H #define CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_ONLY_CHECKER_H -#include "incremental_goto_checker.h" +#include #include -#include - +#include "incremental_goto_checker.h" #include "symex_bmc.h" class multi_path_symex_only_checkert : public incremental_goto_checkert diff --git a/src/goto-checker/single_loop_incremental_symex_checker.h b/src/goto-checker/single_loop_incremental_symex_checker.h index bcf469b70fe..e5fd98bde13 100644 --- a/src/goto-checker/single_loop_incremental_symex_checker.h +++ b/src/goto-checker/single_loop_incremental_symex_checker.h @@ -14,9 +14,9 @@ Author: Daniel Kroening, Peter Schrammel #ifndef CPROVER_GOTO_CHECKER_SINGLE_LOOP_INCREMENTAL_SYMEX_CHECKER_H #define CPROVER_GOTO_CHECKER_SINGLE_LOOP_INCREMENTAL_SYMEX_CHECKER_H -#include +#include -#include +#include #include "goto_symex_property_decider.h" #include "goto_trace_provider.h" diff --git a/src/goto-checker/single_path_symex_only_checker.h b/src/goto-checker/single_path_symex_only_checker.h index 325459e919c..aee94cbbb68 100644 --- a/src/goto-checker/single_path_symex_only_checker.h +++ b/src/goto-checker/single_path_symex_only_checker.h @@ -12,7 +12,8 @@ Author: Daniel Kroening, Peter Schrammel #ifndef CPROVER_GOTO_CHECKER_SINGLE_PATH_SYMEX_ONLY_CHECKER_H #define CPROVER_GOTO_CHECKER_SINGLE_PATH_SYMEX_ONLY_CHECKER_H -#include +#include + #include #include "incremental_goto_checker.h" diff --git a/src/goto-checker/symex_bmc.cpp b/src/goto-checker/symex_bmc.cpp index 56bd0c198d6..de4ecdd28b4 100644 --- a/src/goto-checker/symex_bmc.cpp +++ b/src/goto-checker/symex_bmc.cpp @@ -11,12 +11,12 @@ Author: Daniel Kroening, kroening@kroening.com #include "symex_bmc.h" -#include - #include #include -#include +#include + +#include symex_bmct::symex_bmct( message_handlert &mh, diff --git a/src/goto-checker/symex_bmc_incremental_one_loop.cpp b/src/goto-checker/symex_bmc_incremental_one_loop.cpp index 7003f4ef30d..0492797d6a6 100644 --- a/src/goto-checker/symex_bmc_incremental_one_loop.cpp +++ b/src/goto-checker/symex_bmc_incremental_one_loop.cpp @@ -6,13 +6,13 @@ Author: Peter Schrammel, Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include - #include "symex_bmc_incremental_one_loop.h" #include -#include +#include + +#include symex_bmc_incremental_one_loopt::symex_bmc_incremental_one_loopt( message_handlert &message_handler, diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index b33c52692f0..7349fe8bc31 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -99,7 +99,6 @@ SRC = accelerate/accelerate.cpp \ undefined_functions.cpp \ uninitialized.cpp \ unwind.cpp \ - unwindset.cpp \ value_set_fi_fp_removal.cpp \ wmm/abstract_event.cpp \ wmm/cycle_collection.cpp \ diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index f99d87e4477..8cb69c96ed8 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -27,13 +27,13 @@ Date: February 2016 #include #include #include +#include #include #include #include #include #include -#include #include #include "cfg_info.h" diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp index 4b7302cd2c2..2bc0e1536cf 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp @@ -20,13 +20,13 @@ Author: Remi Delmas, delmarsd@amazon.com #include #include +#include #include #include #include #include #include -#include #include #include "dfcc_cfg_info.h" diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp index f9a5f51c2fe..5c8e8f2fb38 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp @@ -20,6 +20,7 @@ Author: Remi Delmas, delmarsd@amazon.com #include #include +#include #include #include @@ -27,7 +28,6 @@ Author: Remi Delmas, delmarsd@amazon.com #include #include #include -#include #include #include "dfcc_utils.h" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 5258481c270..1927f49e2bc 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -24,6 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -39,7 +40,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "reachability_slicer.h" #include "replace_calls.h" #include "uninitialized.h" -#include "unwindset.h" #include "contracts/contracts.h" #include "contracts/contracts_wrangler.h" diff --git a/src/goto-instrument/unwind.cpp b/src/goto-instrument/unwind.cpp index c52adcdd905..c99e19f2280 100644 --- a/src/goto-instrument/unwind.cpp +++ b/src/goto-instrument/unwind.cpp @@ -20,8 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include - -#include "unwindset.h" +#include void goto_unwindt::copy_segment( const goto_programt::const_targett start, diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index 21b06168563..bacc92ac152 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -56,6 +56,7 @@ SRC = adjust_float_expressions.cpp \ string_abstraction.cpp \ structured_trace_util.cpp \ system_library_symbols.cpp \ + unwindset.cpp \ validate_code.cpp \ validate_goto_model.cpp \ vcd_goto_trace.cpp \ diff --git a/src/goto-instrument/unwindset.cpp b/src/goto-programs/unwindset.cpp similarity index 98% rename from src/goto-instrument/unwindset.cpp rename to src/goto-programs/unwindset.cpp index 7dc097efd03..4d112e49f28 100644 --- a/src/goto-instrument/unwindset.cpp +++ b/src/goto-programs/unwindset.cpp @@ -15,7 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include "abstract_goto_model.h" #include #include @@ -216,7 +216,7 @@ void unwindsett::parse_unwindset_file( std::ifstream file(widen_if_needed(file_name)); if(!file) - throw "cannot open file "+file_name; + throw "cannot open file " + file_name; std::stringstream buffer; buffer << file.rdbuf(); diff --git a/src/goto-instrument/unwindset.h b/src/goto-programs/unwindset.h similarity index 100% rename from src/goto-instrument/unwindset.h rename to src/goto-programs/unwindset.h diff --git a/src/goto-synthesizer/Makefile b/src/goto-synthesizer/Makefile index 53d634021e3..8b85a230c80 100644 --- a/src/goto-synthesizer/Makefile +++ b/src/goto-synthesizer/Makefile @@ -26,7 +26,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../goto-instrument/loop_utils$(OBJEXT) \ ../goto-instrument/nondet_static$(OBJEXT) \ ../goto-instrument/unwind$(OBJEXT) \ - ../goto-instrument/unwindset$(OBJEXT) \ ../goto-symex/goto-symex$(LIBEXT) \ ../json/json$(LIBEXT) \ ../langapi/langapi$(LIBEXT) \ diff --git a/src/libcprover-cpp/Makefile b/src/libcprover-cpp/Makefile index 54746d50058..d1d05f89c09 100644 --- a/src/libcprover-cpp/Makefile +++ b/src/libcprover-cpp/Makefile @@ -25,7 +25,6 @@ OBJ += \ ../goto-instrument/nondet_static$(OBJEXT) \ ../goto-instrument/reachability_slicer$(OBJEXT) \ ../goto-instrument/source_lines$(OBJEXT) \ - ../goto-instrument/unwindset$(OBJEXT) \ ../goto-programs/goto-programs$(LIBEXT) \ ../goto-symex/goto-symex$(LIBEXT) \ ../json-symtab-language/json-symtab-language$(LIBEXT) \ diff --git a/unit/Makefile b/unit/Makefile index ebd38a5aa4b..bc93e74a34c 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -260,7 +260,6 @@ BMC_DEPS =../src/cbmc/c_test_input_generator$(OBJEXT) \ ../src/goto-instrument/reachability_slicer$(OBJEXT) \ ../src/goto-instrument/nondet_static$(OBJEXT) \ ../src/goto-instrument/full_slicer$(OBJEXT) \ - ../src/goto-instrument/unwindset$(OBJEXT) \ ../src/goto-synthesizer/expr_enumerator$(OBJEXT) \ ../src/xmllang/xmllang$(LIBEXT) \ ../src/goto-symex/goto-symex$(LIBEXT) \ diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp index 4b9ff978e99..e118a684be7 100644 --- a/unit/path_strategies.cpp +++ b/unit/path_strategies.cpp @@ -6,31 +6,25 @@ Author: Kareem Khazem , 2018 \*******************************************************************/ -#include +#include +#include +#include -#include - -#include -#include -#include +#include #include - #include - #include #include #include - #include - -#include - #include +#include -#include -#include -#include +#include +#include +#include +#include // The actual test suite. //