From 9c03ca3fd34bd6574169af89ccd97420578f495b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 26 Apr 2018 18:18:49 +0000 Subject: [PATCH 1/8] Use iosfwd instead of ostream where possible --- src/analyses/goto_rw.h | 2 +- src/cbmc/symex_coverage.h | 2 +- src/goto-analyzer/static_show_domain.h | 2 +- src/goto-analyzer/static_simplifier.h | 2 +- src/goto-analyzer/static_verifier.h | 2 +- src/goto-instrument/object_id.h | 2 +- src/jsil/jsil_parse_tree.cpp | 2 ++ src/jsil/jsil_parse_tree.h | 2 +- src/util/graph.h | 2 +- src/util/json_stream.h | 2 +- src/util/string_utils.h | 2 +- src/xmllang/graphml.h | 3 +-- 12 files changed, 13 insertions(+), 12 deletions(-) diff --git a/src/analyses/goto_rw.h b/src/analyses/goto_rw.h index 02f17a7af16..bc1c848413f 100644 --- a/src/analyses/goto_rw.h +++ b/src/analyses/goto_rw.h @@ -13,7 +13,7 @@ Date: April 2010 #define CPROVER_ANALYSES_GOTO_RW_H #include -#include +#include #include #include // unique_ptr diff --git a/src/cbmc/symex_coverage.h b/src/cbmc/symex_coverage.h index b7556b1087b..9bba52fd84b 100644 --- a/src/cbmc/symex_coverage.h +++ b/src/cbmc/symex_coverage.h @@ -15,7 +15,7 @@ Date: March 2016 #define CPROVER_CBMC_SYMEX_COVERAGE_H #include -#include +#include #include #include diff --git a/src/goto-analyzer/static_show_domain.h b/src/goto-analyzer/static_show_domain.h index 5284cc6a9ec..1b2c3ee3772 100644 --- a/src/goto-analyzer/static_show_domain.h +++ b/src/goto-analyzer/static_show_domain.h @@ -9,7 +9,7 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk #ifndef CPROVER_GOTO_ANALYZER_STATIC_SHOW_DOMAIN_H #define CPROVER_GOTO_ANALYZER_STATIC_SHOW_DOMAIN_H -#include +#include #include #include diff --git a/src/goto-analyzer/static_simplifier.h b/src/goto-analyzer/static_simplifier.h index ee810bf8793..59e741fba83 100644 --- a/src/goto-analyzer/static_simplifier.h +++ b/src/goto-analyzer/static_simplifier.h @@ -9,7 +9,7 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk #ifndef CPROVER_GOTO_ANALYZER_STATIC_SIMPLIFIER_H #define CPROVER_GOTO_ANALYZER_STATIC_SIMPLIFIER_H -#include +#include #include #include diff --git a/src/goto-analyzer/static_verifier.h b/src/goto-analyzer/static_verifier.h index 77eeacbe527..e71bdfbb45c 100644 --- a/src/goto-analyzer/static_verifier.h +++ b/src/goto-analyzer/static_verifier.h @@ -9,7 +9,7 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk #ifndef CPROVER_GOTO_ANALYZER_STATIC_VERIFIER_H #define CPROVER_GOTO_ANALYZER_STATIC_VERIFIER_H -#include +#include #include #include diff --git a/src/goto-instrument/object_id.h b/src/goto-instrument/object_id.h index f7c597a798b..98e4b03033b 100644 --- a/src/goto-instrument/object_id.h +++ b/src/goto-instrument/object_id.h @@ -13,7 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_GOTO_INSTRUMENT_OBJECT_ID_H #include -#include +#include #include #include diff --git a/src/jsil/jsil_parse_tree.cpp b/src/jsil/jsil_parse_tree.cpp index 093a62f4fb9..8263b843c98 100644 --- a/src/jsil/jsil_parse_tree.cpp +++ b/src/jsil/jsil_parse_tree.cpp @@ -11,6 +11,8 @@ Author: Michael Tautschnig, tautschn@amazon.com #include "jsil_parse_tree.h" +#include + #include #include "jsil_types.h" diff --git a/src/jsil/jsil_parse_tree.h b/src/jsil/jsil_parse_tree.h index 55ee57de51b..f5410564783 100644 --- a/src/jsil/jsil_parse_tree.h +++ b/src/jsil/jsil_parse_tree.h @@ -12,7 +12,7 @@ Author: Michael Tautschnig, tautschn@amazon.com #ifndef CPROVER_JSIL_JSIL_PARSE_TREE_H #define CPROVER_JSIL_JSIL_PARSE_TREE_H -#include +#include #include #include diff --git a/src/util/graph.h b/src/util/graph.h index 16af29ea634..85ad33c448d 100644 --- a/src/util/graph.h +++ b/src/util/graph.h @@ -16,7 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include +#include #include #include #include diff --git a/src/util/json_stream.h b/src/util/json_stream.h index 4f1541d0496..f27e360c9a3 100644 --- a/src/util/json_stream.h +++ b/src/util/json_stream.h @@ -10,7 +10,7 @@ Author: Peter Schrammel #define CPROVER_UTIL_JSON_STREAM_H #include -#include +#include #include "json.h" #include "invariant.h" diff --git a/src/util/string_utils.h b/src/util/string_utils.h index 87dd742d666..23d3d6ea6ba 100644 --- a/src/util/string_utils.h +++ b/src/util/string_utils.h @@ -10,7 +10,7 @@ Author: Daniel Poetzl #ifndef CPROVER_UTIL_STRING_UTILS_H #define CPROVER_UTIL_STRING_UTILS_H -#include +#include #include #include diff --git a/src/xmllang/graphml.h b/src/xmllang/graphml.h index 3b399d48c3b..f86dac5648e 100644 --- a/src/xmllang/graphml.h +++ b/src/xmllang/graphml.h @@ -12,8 +12,7 @@ Author: Michael Tautschnig, mt@eecs.qmul.ac.uk #ifndef CPROVER_XMLLANG_GRAPHML_H #define CPROVER_XMLLANG_GRAPHML_H -#include -#include +#include #include #include From d351a5d094ec4b3ead4a3f5c6e139443ae936737 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 26 Apr 2018 18:21:43 +0000 Subject: [PATCH 2/8] Use a single global INITIALIZE_FUNCTION macro instead of __CPROVER_initialize --- src/ansi-c/ansi_c_entry_point.cpp | 3 ++- src/ansi-c/ansi_c_internal_additions.cpp | 4 +++- src/cbmc/bmc.cpp | 4 +++- src/cbmc/symex_coverage.cpp | 4 +++- src/cpp/cpp_internal_additions.cpp | 4 +++- src/goto-cc/compile.cpp | 4 +++- src/goto-cc/linker_script_merge.cpp | 7 ++++--- src/goto-instrument/call_sequences.cpp | 4 +++- src/goto-instrument/code_contracts.cpp | 4 +++- src/goto-instrument/cover_filter.cpp | 6 ++---- src/goto-instrument/dump_c.cpp | 4 +++- src/goto-instrument/interrupt.cpp | 12 ++---------- src/goto-instrument/mmio.cpp | 4 ++-- src/goto-instrument/nondet_static.cpp | 4 +++- src/goto-instrument/race_check.cpp | 4 +++- src/goto-instrument/stack_depth.cpp | 11 ++++++----- src/goto-instrument/wmm/goto2graph.cpp | 4 +++- src/goto-instrument/wmm/shared_buffers.cpp | 5 ++++- src/goto-instrument/wmm/weak_memory.cpp | 4 +++- src/java_bytecode/java_entry_point.cpp | 3 ++- src/jsil/jsil_entry_point.cpp | 12 ++++++------ src/linking/remove_internal_symbols.cpp | 4 +++- 22 files changed, 69 insertions(+), 46 deletions(-) diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index a632d616fc2..04da6131608 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -23,6 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include + #include #include "c_nondet_symbol_factory.h" @@ -217,7 +218,7 @@ bool generate_ansi_c_start_function( if(init_it==symbol_table.symbols.end()) { messaget message(message_handler); - message.error() << "failed to find " CPROVER_PREFIX "initialize symbol" + message.error() << "failed to find " INITIALIZE_FUNCTION " symbol" << messaget::eom; return true; } diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index 845e2197e84..47ef1c503f5 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -10,6 +10,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include + const char gcc_builtin_headers_types[]= "# 1 \"gcc_builtin_headers_types.h\"\n" #include "gcc_builtin_headers_types.inc" @@ -172,7 +174,7 @@ void ansi_c_internal_additions(std::string &code) "\n" // This function needs to be declared, or otherwise can't be called // by the entry-point construction. - "void __CPROVER_initialize(void);\n" + "void " INITIALIZE_FUNCTION "(void);\n" "\n"; // GCC junk stuff, also for CLANG and ARM diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 37bedbed2f4..e0af60274f5 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -42,6 +42,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include "cbmc_solvers.h" #include "counterexample_beautification.h" #include "fault_localization.h" @@ -338,7 +340,7 @@ void bmct::setup() { const symbolt *init_symbol; - if(!ns.lookup(CPROVER_PREFIX "initialize", init_symbol)) + if(!ns.lookup(INITIALIZE_FUNCTION, init_symbol)) symex.language_mode=init_symbol->mode; } diff --git a/src/cbmc/symex_coverage.cpp b/src/cbmc/symex_coverage.cpp index fec36dd1f5f..77f7fe93ba6 100644 --- a/src/cbmc/symex_coverage.cpp +++ b/src/cbmc/symex_coverage.cpp @@ -29,6 +29,8 @@ Date: March 2016 #include #include +#include + class coverage_recordt { public: @@ -313,7 +315,7 @@ void symex_coveraget::compute_overall_coverage( { if(!gf_it->second.body_available() || gf_it->first==goto_functions.entry_point() || - gf_it->first==CPROVER_PREFIX "initialize") + gf_it->first == INITIALIZE_FUNCTION) continue; goto_program_coverage_recordt func_cov(ns, gf_it, coverage); diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp index 19260f6ac24..85363a59b69 100644 --- a/src/cpp/cpp_internal_additions.cpp +++ b/src/cpp/cpp_internal_additions.cpp @@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include + std::string c2cpp(const std::string &s) { std::string result; @@ -75,7 +77,7 @@ void cpp_internal_additions(std::ostream &out) // CPROVER extensions out << "extern \"C\" const unsigned __CPROVER::constant_infinity_uint;\n"; - out << "extern \"C\" void __CPROVER_initialize();" << '\n'; + out << "extern \"C\" void " INITIALIZE_FUNCTION "();" << '\n'; out << "extern \"C\" void __CPROVER::input(const char *id, ...);" << '\n'; out << "extern \"C\" void __CPROVER::output(const char *id, ...);" << '\n'; out << "extern \"C\" void __CPROVER::cover(bool condition);" << '\n'; diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 4f84f36bc3f..c092f940f95 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -41,6 +41,8 @@ Date: June 2006 #include +#include + #include #define DOTGRAPHSETTINGS "color=black;" \ @@ -372,7 +374,7 @@ bool compilet::link() // new symbols may have been added to a previously linked file // make sure a new entry point is created that contains all // static initializers - compiled_functions.function_map.erase("__CPROVER_initialize"); + compiled_functions.function_map.erase(INITIALIZE_FUNCTION); symbol_table.remove(goto_functionst::entry_point()); compiled_functions.function_map.erase(goto_functionst::entry_point()); diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp index 72ec71f7ad3..c7ede967768 100644 --- a/src/goto-cc/linker_script_merge.cpp +++ b/src/goto-cc/linker_script_merge.cpp @@ -24,6 +24,7 @@ Author: Kareem Khazem , 2017 #include #include +#include #include #include @@ -78,10 +79,10 @@ int linker_script_merget::add_linker_script_definitions() fail=1; linker_valuest linker_values; - const auto &pair=original_gf.function_map.find(CPROVER_PREFIX "initialize"); + const auto &pair=original_gf.function_map.find(INITIALIZE_FUNCTION); if(pair==original_gf.function_map.end()) { - error() << "No " << CPROVER_PREFIX "initialize found in goto_functions" + error() << "No " << INITIALIZE_FUNCTION << " found in goto_functions" << eom; return fail; } @@ -93,7 +94,7 @@ int linker_script_merget::add_linker_script_definitions() linker_values); if(fail!=0) { - error() << "Could not add linkerscript defs to __CPROVER_initialize" << eom; + error() << "Could not add linkerscript defs to " INITIALIZE_FUNCTION << eom; return fail; } diff --git a/src/goto-instrument/call_sequences.cpp b/src/goto-instrument/call_sequences.cpp index c188828768b..82da31087b8 100644 --- a/src/goto-instrument/call_sequences.cpp +++ b/src/goto-instrument/call_sequences.cpp @@ -24,6 +24,8 @@ Date: April 2013 #include +#include + void show_call_sequences( const irep_idt &caller, const goto_programt &goto_program) @@ -286,7 +288,7 @@ static void list_calls_and_arguments( continue; const irep_idt &identifier=to_symbol_expr(f).get_identifier(); - if(identifier=="__CPROVER_initialize") + if(identifier == INITIALIZE_FUNCTION) continue; std::string name=from_expr(ns, identifier, f); diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 256149084eb..16f3ebe8312 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -21,6 +21,8 @@ Date: February 2016 #include +#include + #include "loop_utils.h" class code_contractst @@ -385,7 +387,7 @@ void code_contractst::operator()() code_contracts(it->second); goto_functionst::function_mapt::iterator i_it= - goto_functions.function_map.find(CPROVER_PREFIX "initialize"); + goto_functions.function_map.find(INITIALIZE_FUNCTION); assert(i_it!=goto_functions.function_map.end()); for(const auto &contract : summarized) diff --git a/src/goto-instrument/cover_filter.cpp b/src/goto-instrument/cover_filter.cpp index 3ca83843170..2c9c6c3f6d6 100644 --- a/src/goto-instrument/cover_filter.cpp +++ b/src/goto-instrument/cover_filter.cpp @@ -11,9 +11,7 @@ Author: Peter Schrammel #include "cover_filter.h" -#include - -#include +#include /// Filter out functions that are not considered provided by the user /// \param identifier: a function name @@ -26,7 +24,7 @@ bool internal_functions_filtert::operator()( if(identifier == goto_functionst::entry_point()) return false; - if(identifier == (CPROVER_PREFIX "initialize")) + if(identifier == INITIALIZE_FUNCTION) return false; if(goto_function.is_hidden()) diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index c36cca90179..c51a6859d3e 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -26,6 +26,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include "goto_program2code.h" #include "dump_c_class.h" @@ -953,7 +955,7 @@ void dump_ct::cleanup_harness(code_blockt &b) symbol_exprt &s=to_symbol_expr(func); if(s.get_identifier()==ID_main) s.set_identifier(CPROVER_PREFIX+id2string(ID_main)); - else if(s.get_identifier()==CPROVER_PREFIX "initialize") + else if(s.get_identifier() == INITIALIZE_FUNCTION) continue; } } diff --git a/src/goto-instrument/interrupt.cpp b/src/goto-instrument/interrupt.cpp index 23bf63eb1a4..4d3416a3b38 100644 --- a/src/goto-instrument/interrupt.cpp +++ b/src/goto-instrument/interrupt.cpp @@ -13,15 +13,7 @@ Date: September 2011 #include "interrupt.h" -#include -#include -#include -#include -#include - -#include - -#include "rw_set.h" +#include #ifdef LOCAL_MAY #include @@ -203,7 +195,7 @@ void interrupt( // now instrument Forall_goto_functions(f_it, goto_model.goto_functions) - if(f_it->first!=CPROVER_PREFIX "initialize" && + if(f_it->first != INITIALIZE_FUNCTION && f_it->first!=goto_functionst::entry_point() && f_it->first!=isr.get_identifier()) interrupt( diff --git a/src/goto-instrument/mmio.cpp b/src/goto-instrument/mmio.cpp index e818e9c4ec8..db9df4293fe 100644 --- a/src/goto-instrument/mmio.cpp +++ b/src/goto-instrument/mmio.cpp @@ -13,7 +13,7 @@ Date: September 2011 #include "mmio.h" -#include +#include #include #include @@ -169,7 +169,7 @@ void mmio( // now instrument Forall_goto_functions(f_it, goto_model.goto_functions) - if(f_it->first!=CPROVER_PREFIX "initialize" && + if(f_it->first != INITIALIZE_FUNCTION && f_it->first!=goto_functionst::entry_point()) mmio(value_sets, goto_model.symbol_table, #ifdef LOCAL_MAY diff --git a/src/goto-instrument/nondet_static.cpp b/src/goto-instrument/nondet_static.cpp index 587b935f80a..2dce04f9d22 100644 --- a/src/goto-instrument/nondet_static.cpp +++ b/src/goto-instrument/nondet_static.cpp @@ -22,6 +22,8 @@ Date: November 2011 #include #include +#include + void nondet_static( const namespacet &ns, goto_functionst &goto_functions, @@ -75,7 +77,7 @@ void nondet_static( const namespacet &ns, goto_functionst &goto_functions) { - nondet_static(ns, goto_functions, CPROVER_PREFIX "initialize"); + nondet_static(ns, goto_functions, INITIALIZE_FUNCTION); // update counters etc. goto_functions.update(); diff --git a/src/goto-instrument/race_check.cpp b/src/goto-instrument/race_check.cpp index b426c98815e..8517e90f1ae 100644 --- a/src/goto-instrument/race_check.cpp +++ b/src/goto-instrument/race_check.cpp @@ -25,6 +25,8 @@ Date: February 2006 #include #include +#include + #include "rw_set.h" #ifdef LOCAL_MAY @@ -300,7 +302,7 @@ void race_check( Forall_goto_functions(f_it, goto_model.goto_functions) if(f_it->first!=goto_functionst::entry_point() && - f_it->first!=CPROVER_PREFIX "initialize") + f_it->first != INITIALIZE_FUNCTION) race_check( value_sets, goto_model.symbol_table, diff --git a/src/goto-instrument/stack_depth.cpp b/src/goto-instrument/stack_depth.cpp index 606a25f40bb..a0e0457fa24 100644 --- a/src/goto-instrument/stack_depth.cpp +++ b/src/goto-instrument/stack_depth.cpp @@ -22,6 +22,8 @@ Date: November 2011 #include +#include + symbol_exprt add_stack_depth_symbol(symbol_tablet &symbol_table) { const irep_idt identifier="$stack_depth"; @@ -94,17 +96,16 @@ void stack_depth( Forall_goto_functions(f_it, goto_model.goto_functions) if(f_it->second.body_available() && - f_it->first!=CPROVER_PREFIX "initialize" && + f_it->first != INITIALIZE_FUNCTION && f_it->first!=goto_functionst::entry_point()) stack_depth(f_it->second.body, sym, depth, depth_expr); // initialize depth to 0 - goto_functionst::function_mapt::iterator - i_it=goto_model.goto_functions.function_map.find( - CPROVER_PREFIX "initialize"); + goto_functionst::function_mapt::iterator i_it = + goto_model.goto_functions.function_map.find(INITIALIZE_FUNCTION); DATA_INVARIANT( i_it!=goto_model.goto_functions.function_map.end(), - "__CPROVER_initialize must exist"); + INITIALIZE_FUNCTION " must exist"); goto_programt &init=i_it->second.body; goto_programt::targett first=init.instructions.begin(); diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp index 13587974058..9611f56d2f7 100644 --- a/src/goto-instrument/wmm/goto2graph.cpp +++ b/src/goto-instrument/wmm/goto2graph.cpp @@ -28,6 +28,8 @@ Date: 2012 #include #include +#include + #include "../rw_set.h" #include "fence.h" @@ -168,7 +170,7 @@ void instrumentert::cfg_visitort::visit_cfg_function( instrumenter.message.debug() << "visit function " << function << messaget::eom; - if(function==CPROVER_PREFIX "initialize") + if(function == INITIALIZE_FUNCTION) { return; } diff --git a/src/goto-instrument/wmm/shared_buffers.cpp b/src/goto-instrument/wmm/shared_buffers.cpp index bf78d1ac742..4f8a5e65247 100644 --- a/src/goto-instrument/wmm/shared_buffers.cpp +++ b/src/goto-instrument/wmm/shared_buffers.cpp @@ -7,6 +7,9 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ #include "shared_buffers.h" + +#include + #include "fence.h" #include "../rw_set.h" @@ -1054,7 +1057,7 @@ void shared_bufferst::cfg_visitort::weak_memory( { shared_buffers.message.debug() << "visit function "<< function << messaget::eom; - if(function==CPROVER_PREFIX "initialize") + if(function == INITIALIZE_FUNCTION) return; namespacet ns(symbol_table); diff --git a/src/goto-instrument/wmm/weak_memory.cpp b/src/goto-instrument/wmm/weak_memory.cpp index 468d944f14a..1f2e38b61da 100644 --- a/src/goto-instrument/wmm/weak_memory.cpp +++ b/src/goto-instrument/wmm/weak_memory.cpp @@ -29,6 +29,8 @@ Date: September 2011 #include +#include + #include "../rw_set.h" #include "shared_buffers.h" @@ -135,7 +137,7 @@ void weak_memory( // all access to shared variables is pushed into assignments Forall_goto_functions(f_it, goto_model.goto_functions) - if(f_it->first!=CPROVER_PREFIX "initialize" && + if(f_it->first != INITIALIZE_FUNCTION && f_it->first!=goto_functionst::entry_point()) introduce_temporaries(value_sets, goto_model.symbol_table, f_it->first, f_it->second.body, diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index 1597868caf2..ef4a4e70cc8 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -29,7 +29,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include "remove_exceptions.h" +#include + #include "java_object_factory.h" #include "java_types.h" #include "java_utils.h" diff --git a/src/jsil/jsil_entry_point.cpp b/src/jsil/jsil_entry_point.cpp index 991ca1c226c..a8f1278e961 100644 --- a/src/jsil/jsil_entry_point.cpp +++ b/src/jsil/jsil_entry_point.cpp @@ -20,13 +20,13 @@ Author: Michael Tautschnig, tautschn@amazon.com #include -#define INITIALIZE CPROVER_PREFIX "initialize" +#include static void create_initialize(symbol_tablet &symbol_table) { symbolt initialize; - initialize.name=CPROVER_PREFIX "initialize"; - initialize.base_name=CPROVER_PREFIX "initialize"; + initialize.name = INITIALIZE_FUNCTION; + initialize.base_name = INITIALIZE_FUNCTION; initialize.mode="jsil"; code_typet type; @@ -46,7 +46,7 @@ static void create_initialize(symbol_tablet &symbol_table) initialize.value=init_code; if(symbol_table.add(initialize)) - throw "failed to add " CPROVER_PREFIX "initialize"; + throw "failed to add " INITIALIZE_FUNCTION; } bool jsil_entry_point( @@ -130,10 +130,10 @@ bool jsil_entry_point( { symbol_tablet::symbolst::const_iterator init_it= - symbol_table.symbols.find(CPROVER_PREFIX "initialize"); + symbol_table.symbols.find(INITIALIZE_FUNCTION); if(init_it==symbol_table.symbols.end()) - throw "failed to find " CPROVER_PREFIX "initialize symbol"; + throw "failed to find " INITIALIZE_FUNCTION " symbol"; code_function_callt call_init; call_init.lhs().make_nil(); diff --git a/src/linking/remove_internal_symbols.cpp b/src/linking/remove_internal_symbols.cpp index 11037431b66..91f6e3c411d 100644 --- a/src/linking/remove_internal_symbols.cpp +++ b/src/linking/remove_internal_symbols.cpp @@ -18,6 +18,8 @@ Author: Daniel Kroening #include #include +#include "static_lifetime_init.h" + void get_symbols_rec( const namespacet &ns, const symbolt &symbol, @@ -84,7 +86,7 @@ void remove_internal_symbols( special.insert("envp'"); special.insert("envp_size'"); special.insert(CPROVER_PREFIX "memory"); - special.insert(CPROVER_PREFIX "initialize"); + special.insert(INITIALIZE_FUNCTION); special.insert(CPROVER_PREFIX "malloc_size"); special.insert(CPROVER_PREFIX "deallocated"); special.insert(CPROVER_PREFIX "dead_object"); From 73e0c0f019535f183137bb03a13bab97521ce3e8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 26 Apr 2018 18:27:33 +0000 Subject: [PATCH 3/8] Use C++ streams instead of C-style snprintf --- src/ansi-c/expr2c.cpp | 15 ++++----------- 1 file changed, 4 insertions(+), 11 deletions(-) diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 9a8a06ea799..f309f9be7ec 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -10,14 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include -#include - -#ifdef _WIN32 -#ifndef __MINGW32__ -#define snprintf sprintf_s -#endif -#endif +#include #include #include @@ -2258,9 +2251,9 @@ std::string expr2ct::convert_array( dest+=static_cast(ch); else { - char hexbuf[10]; - snprintf(hexbuf, sizeof(hexbuf), "\\x%x", ch); - dest+=hexbuf; + std::ostringstream oss; + oss << "\\x" << std::hex << ch; + dest += oss.str(); last_was_hex=true; } } From 3af3d724318db85ecdd0dc75870124006c288d42 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 26 Apr 2018 19:13:01 +0000 Subject: [PATCH 4/8] Do not unnecessarily use C string functions --- src/goto-programs/interpreter_evaluate.cpp | 9 +++------ src/goto-programs/string_abstraction.cpp | 10 ++++++++-- 2 files changed, 11 insertions(+), 8 deletions(-) diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp index bb9ea793d0a..15db12bde80 100644 --- a/src/goto-programs/interpreter_evaluate.cpp +++ b/src/goto-programs/interpreter_evaluate.cpp @@ -389,14 +389,11 @@ void interpretert::evaluate( } else if(expr.type().id()==ID_string) { - irep_idt value=to_constant_expr(expr).get_value(); - const char *str=value.c_str(); - std::size_t length=strlen(str)+1; + const std::string &value = id2string(to_constant_expr(expr).get_value()); if(show) warning() << "string decoding not fully implemented " - << length << eom; - mp_integer tmp = get_string_container()[id2string(value)]; - dest.push_back(tmp); + << value.size() + 1 << eom; + dest.push_back(get_string_container()[value]); return; } else diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp index bf97e4c0c5d..fd5a123c6df 100644 --- a/src/goto-programs/string_abstraction.cpp +++ b/src/goto-programs/string_abstraction.cpp @@ -11,8 +11,10 @@ Author: Daniel Kroening, kroening@kroening.com #include "string_abstraction.h" -#include +#include +#include +#include #include #include #include @@ -759,7 +761,11 @@ bool string_abstractiont::build(const exprt &object, exprt &dest, bool write) if(object.id()==ID_string_constant) { - mp_integer str_len=strlen(object.get(ID_value).c_str()); + const std::string &str_value = id2string(object.get(ID_value)); + // make sure we handle the case of a string constant with string-terminating + // \0 in it + const std::size_t str_len = + std::min(str_value.size(), str_value.find('\0')); return build_symbol_constant(str_len, str_len+1, dest); } From 99755fee5c0153b64e1fc2bd3b38369fc4d68a78 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 26 Apr 2018 18:30:28 +0000 Subject: [PATCH 5/8] Move asserts to invariants (and provide suitable includes) --- src/cpp/cpp_exception_id.cpp | 4 +++- src/cpp/cpp_name.h | 5 +++-- src/cpp/cpp_template_args.h | 9 +++++---- src/cpp/cpp_template_type.h | 5 +++-- src/cpp/cpp_token_buffer.h | 4 +++- src/cpp/template_map.cpp | 5 +++-- src/util/typecheck.cpp | 5 +++-- 7 files changed, 23 insertions(+), 14 deletions(-) diff --git a/src/cpp/cpp_exception_id.cpp b/src/cpp/cpp_exception_id.cpp index 23d7f49a30c..aef6606a4bd 100644 --- a/src/cpp/cpp_exception_id.cpp +++ b/src/cpp/cpp_exception_id.cpp @@ -11,6 +11,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "cpp_exception_id.h" +#include + /// turns a type into a list of relevant exception IDs void cpp_exception_list_rec( const typet &src, @@ -91,6 +93,6 @@ irep_idt cpp_exception_id( { std::vector ids; cpp_exception_list_rec(src, ns, "", ids); - assert(!ids.empty()); + CHECK_RETURN(!ids.empty()); return ids.front(); } diff --git a/src/cpp/cpp_name.h b/src/cpp/cpp_name.h index a27374c5524..bb9e1007cf6 100644 --- a/src/cpp/cpp_name.h +++ b/src/cpp/cpp_name.h @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #define CPROVER_CPP_CPP_NAME_H #include +#include class cpp_namet:public irept { @@ -142,13 +143,13 @@ class cpp_namet:public irept inline cpp_namet &to_cpp_name(irept &cpp_name) { - assert(cpp_name.id() == ID_cpp_name); + PRECONDITION(cpp_name.id() == ID_cpp_name); return static_cast(cpp_name); } inline const cpp_namet &to_cpp_name(const irept &cpp_name) { - assert(cpp_name.id() == ID_cpp_name); + PRECONDITION(cpp_name.id() == ID_cpp_name); return static_cast(cpp_name); } diff --git a/src/cpp/cpp_template_args.h b/src/cpp/cpp_template_args.h index 47ceca5f003..22018dfaad4 100644 --- a/src/cpp/cpp_template_args.h +++ b/src/cpp/cpp_template_args.h @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #define CPROVER_CPP_CPP_TEMPLATE_ARGS_H #include +#include // A data structures for template arguments, i.e., // a sequence of types/expressions of the form . @@ -47,14 +48,14 @@ class cpp_template_args_non_tct:public cpp_template_args_baset inline cpp_template_args_non_tct &to_cpp_template_args_non_tc( irept &irep) { - assert(irep.id()==ID_template_args); + PRECONDITION(irep.id() == ID_template_args); return static_cast(irep); } inline const cpp_template_args_non_tct &to_cpp_template_args_non_tc( const irept &irep) { - assert(irep.id()==ID_template_args); + PRECONDITION(irep.id() == ID_template_args); return static_cast(irep); } @@ -80,13 +81,13 @@ class cpp_template_args_tct:public cpp_template_args_baset inline cpp_template_args_tct &to_cpp_template_args_tc(irept &irep) { - assert(irep.id()==ID_template_args); + PRECONDITION(irep.id() == ID_template_args); return static_cast(irep); } inline const cpp_template_args_tct &to_cpp_template_args_tc(const irept &irep) { - assert(irep.id()==ID_template_args); + PRECONDITION(irep.id() == ID_template_args); return static_cast(irep); } diff --git a/src/cpp/cpp_template_type.h b/src/cpp/cpp_template_type.h index 57e9d257e1d..de472b41a48 100644 --- a/src/cpp/cpp_template_type.h +++ b/src/cpp/cpp_template_type.h @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #ifndef CPROVER_CPP_CPP_TEMPLATE_TYPE_H #define CPROVER_CPP_CPP_TEMPLATE_TYPE_H +#include #include #include @@ -37,13 +38,13 @@ class template_typet:public typet inline template_typet &to_template_type(typet &type) { - assert(type.id()==ID_template); + PRECONDITION(type.id() == ID_template); return static_cast(type); } inline const template_typet &to_template_type(const typet &type) { - assert(type.id()==ID_template); + PRECONDITION(type.id() == ID_template); return static_cast(type); } diff --git a/src/cpp/cpp_token_buffer.h b/src/cpp/cpp_token_buffer.h index b24f84dbe70..4d3acdbfc3c 100644 --- a/src/cpp/cpp_token_buffer.h +++ b/src/cpp/cpp_token_buffer.h @@ -16,6 +16,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include +#include + class cpp_token_buffert { public: @@ -45,7 +47,7 @@ class cpp_token_buffert // the token that is currently being read from the file cpp_tokent ¤t_token() { - assert(!tokens.empty()); + PRECONDITION(!tokens.empty()); return tokens.back(); } diff --git a/src/cpp/template_map.cpp b/src/cpp/template_map.cpp index 16949d7aaa7..3526603d1dc 100644 --- a/src/cpp/template_map.cpp +++ b/src/cpp/template_map.cpp @@ -173,14 +173,15 @@ void template_mapt::build( } // these should have been typechecked before - assert(instance.size()==template_parameters.size()); + DATA_INVARIANT( + instance.size() == template_parameters.size(), + "template instantiation expected to match declaration"); for(cpp_template_args_tct::argumentst::const_iterator i_it=instance.begin(); i_it!=instance.end(); i_it++, t_it++) { - assert(t_it!=template_parameters.end()); set(*t_it, *i_it); } } diff --git a/src/util/typecheck.cpp b/src/util/typecheck.cpp index a09f54d8ff0..24c57c8a7b7 100644 --- a/src/util/typecheck.cpp +++ b/src/util/typecheck.cpp @@ -6,12 +6,13 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ - #include "typecheck.h" +#include "invariant.h" + bool typecheckt::typecheck_main() { - assert(message_handler); + PRECONDITION(message_handler); const unsigned errors_before= message_handler->get_message_count(messaget::M_ERROR); From 104bc56ff07c064259b161cffb25797dbd52bc9e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 26 Apr 2018 19:15:35 +0000 Subject: [PATCH 6/8] Use pointer_offset_bits instead of locally hacking up what it does anyway --- src/goto-programs/vcd_goto_trace.cpp | 19 ++----------------- .../value_set_dereference.cpp | 18 ++---------------- 2 files changed, 4 insertions(+), 33 deletions(-) diff --git a/src/goto-programs/vcd_goto_trace.cpp b/src/goto-programs/vcd_goto_trace.cpp index 4becb3af583..7acc15e890b 100644 --- a/src/goto-programs/vcd_goto_trace.cpp +++ b/src/goto-programs/vcd_goto_trace.cpp @@ -63,17 +63,7 @@ std::string as_vcd_binary( // build "xxx" - mp_integer width; - - if(type.id()==ID_unsignedbv || - type.id()==ID_signedbv || - type.id()==ID_floatbv || - type.id()==ID_fixedbv || - type.id()==ID_pointer || - type.id()==ID_bv) - width=string2integer(type.get_string(ID_width)); - else - width=pointer_offset_size(type, ns)*8; + const mp_integer width = pointer_offset_bits(type, ns); if(width>=0) return std::string(integer2size_t(width), 'x'); @@ -106,12 +96,7 @@ void output_vcd( const auto number=n.number(identifier); - mp_integer width; - - if(type.id()==ID_bool) - width=1; - else - width=pointer_offset_bits(type, ns); + const mp_integer width = pointer_offset_bits(type, ns); if(width>=1) out << "$var reg " << width << " V" << number << " " diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index 59a62f31cd6..4e437ede5ea 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -712,20 +712,6 @@ void value_set_dereferencet::bounds_check( } } -inline static unsigned bv_width( - const typet &type, - const namespacet &ns) -{ - if(type.id()==ID_c_enum_tag) - { - const typet &t=ns.follow_tag(to_c_enum_tag_type(type)); - assert(t.id()==ID_c_enum); - return bv_width(t.subtype(), ns); - } - - return unsafe_string2unsigned(type.get_string(ID_width)); -} - static bool is_a_bv_type(const typet &type) { return type.id()==ID_unsignedbv || @@ -752,7 +738,7 @@ bool value_set_dereferencet::memory_model( if(is_a_bv_type(from_type) && is_a_bv_type(to_type)) { - if(bv_width(from_type, ns)==bv_width(to_type, ns)) + if(pointer_offset_bits(from_type, ns) == pointer_offset_bits(to_type, ns)) { // avoid semantic conversion in case of // cast to float or fixed-point, @@ -772,7 +758,7 @@ bool value_set_dereferencet::memory_model( if(from_type.id()==ID_pointer && to_type.id()==ID_pointer) { - if(bv_width(from_type, ns)==bv_width(to_type, ns)) + if(pointer_offset_bits(from_type, ns) == pointer_offset_bits(to_type, ns)) return memory_model_conversion(value, to_type, guard, offset); } From b04122ed5258ae36ae6870dac5b3d88ba04d3727 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 26 Apr 2018 19:18:53 +0000 Subject: [PATCH 7/8] Move definition of base_type_eqt to .cpp This is an implementation detail that need not be exposed to users - the interface is the free function base_type_eq. --- src/util/base_type.cpp | 33 +++++++++++++++++++++++++++++++++ src/util/base_type.h | 35 ----------------------------------- 2 files changed, 33 insertions(+), 35 deletions(-) diff --git a/src/util/base_type.cpp b/src/util/base_type.cpp index 62d40ad32e5..4aba15b5505 100644 --- a/src/util/base_type.cpp +++ b/src/util/base_type.cpp @@ -17,6 +17,39 @@ Author: Daniel Kroening, kroening@kroening.com #include "std_types.h" #include "namespace.h" #include "symbol.h" +#include "union_find.h" + +class base_type_eqt +{ +public: + explicit base_type_eqt(const namespacet &_ns):ns(_ns) + { + } + + bool base_type_eq(const typet &type1, const typet &type2) + { + identifiers.clear(); + return base_type_eq_rec(type1, type2); + } + + bool base_type_eq(const exprt &expr1, const exprt &expr2) + { + identifiers.clear(); + return base_type_eq_rec(expr1, expr2); + } + + virtual ~base_type_eqt() { } + +protected: + const namespacet &ns; + + virtual bool base_type_eq_rec(const typet &type1, const typet &type2); + virtual bool base_type_eq_rec(const exprt &expr1, const exprt &expr2); + + // for loop avoidance + typedef union_find identifierst; + identifierst identifiers; +}; void base_type_rec( typet &type, const namespacet &ns, std::set &symb) diff --git a/src/util/base_type.h b/src/util/base_type.h index 833fd855cca..6315ac09542 100644 --- a/src/util/base_type.h +++ b/src/util/base_type.h @@ -12,9 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_BASE_TYPE_H #define CPROVER_UTIL_BASE_TYPE_H -#include "union_find.h" -#include "irep.h" - class exprt; class typet; class namespacet; @@ -29,36 +26,4 @@ bool base_type_eq( const exprt &expr2, const namespacet &ns); -class base_type_eqt -{ -public: - explicit base_type_eqt(const namespacet &_ns):ns(_ns) - { - } - - bool base_type_eq(const typet &type1, const typet &type2) - { - identifiers.clear(); - return base_type_eq_rec(type1, type2); - } - - bool base_type_eq(const exprt &expr1, const exprt &expr2) - { - identifiers.clear(); - return base_type_eq_rec(expr1, expr2); - } - - virtual ~base_type_eqt() { } - -protected: - const namespacet &ns; - - virtual bool base_type_eq_rec(const typet &type1, const typet &type2); - virtual bool base_type_eq_rec(const exprt &expr1, const exprt &expr2); - - // for loop avoidance - typedef union_find identifierst; - identifierst identifiers; -}; - #endif // CPROVER_UTIL_BASE_TYPE_H From a6a825adf1714dd674b3f27719120f2e29a3dc09 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 26 Apr 2018 18:26:42 +0000 Subject: [PATCH 8/8] Remove unused includes ... and sort the remaining ones lexicographically. --- src/analyses/goto_rw.h | 2 +- src/ansi-c/ansi_c_entry_point.cpp | 9 ------ src/ansi-c/c_nondet_symbol_factory.cpp | 8 ------ src/ansi-c/c_typecheck_expr.cpp | 11 +++----- src/ansi-c/c_typecheck_type.cpp | 9 ++---- src/ansi-c/expr2c.cpp | 13 +++------ src/ansi-c/type2name.cpp | 7 ++--- src/cbmc/bmc.cpp | 19 ++----------- src/cbmc/symex_coverage.cpp | 9 ++---- src/cbmc/symex_coverage.h | 2 +- src/cpp/cpp_template_type.h | 1 - src/cpp/cpp_typecheck_expr.cpp | 13 +++------ src/cpp/cpp_typecheck_initializer.cpp | 3 -- src/goto-analyzer/static_show_domain.cpp | 2 ++ src/goto-analyzer/static_show_domain.h | 10 +++---- src/goto-analyzer/static_simplifier.cpp | 14 +++++----- src/goto-analyzer/static_simplifier.h | 10 +++---- src/goto-analyzer/static_verifier.cpp | 9 ++++-- src/goto-analyzer/static_verifier.h | 10 +++---- .../unreachable_instructions.cpp | 12 ++++---- src/goto-analyzer/unreachable_instructions.h | 10 +++---- src/goto-cc/compile.cpp | 14 +++------- src/goto-cc/linker_script_merge.cpp | 15 +++------- src/goto-diff/goto_diff.h | 9 +++--- src/goto-diff/goto_diff_base.cpp | 5 ++-- src/goto-diff/syntactic_diff.cpp | 2 ++ src/goto-instrument/alignment_checks.cpp | 3 +- src/goto-instrument/call_sequences.cpp | 2 -- src/goto-instrument/code_contracts.cpp | 1 - src/goto-instrument/dump_c.cpp | 12 ++------ src/goto-instrument/mmio.cpp | 12 -------- src/goto-instrument/nondet_static.cpp | 6 ---- src/goto-instrument/object_id.h | 2 +- src/goto-instrument/race_check.cpp | 10 ------- src/goto-instrument/rw_set.h | 6 ++-- src/goto-instrument/stack_depth.cpp | 5 ---- src/goto-instrument/wmm/goto2graph.cpp | 9 ------ src/goto-instrument/wmm/shared_buffers.cpp | 6 ++-- src/goto-instrument/wmm/weak_memory.cpp | 4 --- src/goto-programs/builtin_functions.cpp | 9 ------ src/goto-programs/class_hierarchy.h | 4 ++- .../generate_function_bodies.cpp | 9 +----- src/goto-programs/goto_functions.h | 10 +++---- src/goto-programs/goto_program.h | 1 - src/goto-programs/interpreter_evaluate.cpp | 10 ++----- src/goto-programs/remove_asm.cpp | 5 ++-- src/goto-programs/remove_asm.h | 5 +++- src/goto-programs/remove_calls_no_body.cpp | 5 +++- src/goto-programs/remove_calls_no_body.h | 4 ++- src/goto-programs/remove_complex.cpp | 4 +++ src/goto-programs/remove_complex.h | 4 ++- .../remove_const_function_pointers.cpp | 9 ++++-- .../remove_const_function_pointers.h | 17 ++++++++--- src/goto-programs/remove_function_pointers.h | 7 +++-- src/goto-programs/remove_returns.cpp | 3 +- src/goto-programs/remove_returns.h | 9 +++++- src/goto-programs/remove_skip.h | 3 +- src/goto-programs/remove_unreachable.cpp | 2 ++ src/goto-programs/remove_unreachable.h | 3 +- src/goto-programs/remove_unused_functions.cpp | 2 ++ src/goto-programs/remove_unused_functions.h | 9 ++++-- src/goto-programs/remove_vector.cpp | 4 +++ src/goto-programs/remove_vector.h | 4 ++- .../remove_virtual_functions.cpp | 12 ++++---- src/goto-programs/remove_virtual_functions.h | 9 +++++- src/goto-programs/string_abstraction.cpp | 6 ---- src/goto-programs/vcd_goto_trace.cpp | 6 ++-- .../equation_conversion_exceptions.h | 2 +- src/goto-symex/goto_symex.h | 2 +- src/goto-symex/symex_builtin_functions.cpp | 14 ++-------- src/goto-symex/symex_clean_expr.cpp | 5 ++-- src/goto-symex/symex_dereference.cpp | 8 ++---- src/goto-symex/symex_function_call.cpp | 12 ++------ src/goto-symex/symex_other.cpp | 6 +--- src/java_bytecode/java_entry_point.cpp | 20 ++----------- src/java_bytecode/java_object_factory.cpp | 20 +------------ src/jsil/jsil_entry_point.cpp | 3 -- src/linking/linking.cpp | 10 +++---- src/linking/remove_internal_symbols.cpp | 7 ++--- src/linking/static_lifetime_init.h | 7 +++-- src/linking/zero_initializer.cpp | 11 +++----- src/pointer-analysis/value_set.cpp | 12 ++------ .../value_set_dereference.cpp | 24 ++++------------ src/solvers/flattening/boolbv_update.cpp | 6 ---- src/solvers/flattening/bv_pointers.cpp | 6 +--- .../flattening/flatten_byte_operators.cpp | 10 +++---- src/solvers/flattening/pointer_logic.cpp | 5 ++-- src/util/base_type.cpp | 3 +- src/util/fresh_symbol.cpp | 2 ++ src/util/fresh_symbol.h | 10 ++++--- src/util/graph.h | 12 ++++---- src/util/invariant_utils.h | 3 +- src/util/irep.h | 2 -- src/util/irep_hash_container.h | 13 ++++----- src/util/json_irep.h | 2 +- src/util/json_stream.h | 2 +- src/util/nondet_bool.h | 4 +-- src/util/nondet_ifthenelse.h | 2 +- src/util/numbering.h | 5 ++-- src/util/pointer_offset_size.cpp | 10 ++----- src/util/pointer_predicates.cpp | 6 ++-- src/util/rational.h | 3 -- src/util/refined_string_type.cpp | 2 ++ src/util/refined_string_type.h | 7 ++--- src/util/sharing_map.h | 8 ++---- src/util/sharing_node.h | 1 - src/util/simplify_expr.cpp | 28 ++++++++----------- src/util/simplify_expr_array.cpp | 9 ++---- src/util/simplify_expr_int.cpp | 2 -- src/util/simplify_expr_pointer.cpp | 12 ++++---- src/util/simplify_expr_struct.cpp | 9 ++---- src/util/ssa_expr.h | 2 +- src/util/std_expr.cpp | 2 -- src/util/string_expr.h | 6 ++-- src/util/symbol_table_base.h | 4 --- src/util/union_find_replace.h | 2 +- 116 files changed, 308 insertions(+), 536 deletions(-) diff --git a/src/analyses/goto_rw.h b/src/analyses/goto_rw.h index bc1c848413f..d84c6da1964 100644 --- a/src/analyses/goto_rw.h +++ b/src/analyses/goto_rw.h @@ -12,9 +12,9 @@ Date: April 2010 #ifndef CPROVER_ANALYSES_GOTO_RW_H #define CPROVER_ANALYSES_GOTO_RW_H -#include #include #include +#include #include // unique_ptr #include diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index 04da6131608..f15a3124f55 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -8,19 +8,10 @@ Author: Daniel Kroening, kroening@kroening.com #include "ansi_c_entry_point.h" -#include -#include - #include #include #include -#include -#include -#include -#include -#include #include -#include #include diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp index 9b7d88d2bfb..8200e70a84e 100644 --- a/src/ansi-c/c_nondet_symbol_factory.cpp +++ b/src/ansi-c/c_nondet_symbol_factory.cpp @@ -11,22 +11,14 @@ Author: Diffblue Ltd. #include "c_nondet_symbol_factory.h" -#include -#include - #include #include #include #include -#include -#include -#include #include #include #include -#include - #include /// Create a new temporary static symbol diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 5a8eb6cfb4e..b3d7389f995 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -14,17 +14,14 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include -#include -#include -#include #include -#include -#include -#include -#include +#include #include #include +#include +#include #include "builtin_factory.h" #include "c_typecast.h" diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index 1acc58d2f20..dcb40a0e897 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -13,19 +13,16 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include #include #include -#include -#include -#include -#include #include +#include +#include "ansi_c_convert_type.h" #include "c_qualifiers.h" -#include "ansi_c_declaration.h" #include "padding.h" #include "type2name.h" -#include "ansi_c_convert_type.h" void c_typecheck_baset::typecheck_type(typet &type) { diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index f309f9be7ec..305a38e008f 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -13,23 +13,18 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include -#include -#include -#include +#include #include -#include -#include #include +#include #include -#include -#include -#include #include +#include +#include #include "c_misc.h" #include "c_qualifiers.h" diff --git a/src/ansi-c/type2name.cpp b/src/ansi-c/type2name.cpp index 3f1b6e85905..614b46b7ea0 100644 --- a/src/ansi-c/type2name.cpp +++ b/src/ansi-c/type2name.cpp @@ -11,13 +11,12 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "type2name.h" -#include #include +#include #include -#include -#include #include -#include +#include +#include typedef std::unordered_map> symbol_numbert; diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index e0af60274f5..545ab8a54f1 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -12,35 +12,22 @@ Author: Daniel Kroening, kroening@kroening.com #include "bmc.h" #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 #include -#include -#include -#include #include diff --git a/src/cbmc/symex_coverage.cpp b/src/cbmc/symex_coverage.cpp index 77f7fe93ba6..0ecd58b1083 100644 --- a/src/cbmc/symex_coverage.cpp +++ b/src/cbmc/symex_coverage.cpp @@ -13,16 +13,13 @@ Date: March 2016 #include "symex_coverage.h" -#include #include -#include +#include #include -#include +#include -#include #include -#include -#include +#include #include diff --git a/src/cbmc/symex_coverage.h b/src/cbmc/symex_coverage.h index 9bba52fd84b..6eac2cf4ef7 100644 --- a/src/cbmc/symex_coverage.h +++ b/src/cbmc/symex_coverage.h @@ -14,9 +14,9 @@ Date: March 2016 #ifndef CPROVER_CBMC_SYMEX_COVERAGE_H #define CPROVER_CBMC_SYMEX_COVERAGE_H -#include #include #include +#include #include diff --git a/src/cpp/cpp_template_type.h b/src/cpp/cpp_template_type.h index de472b41a48..9c69e6208de 100644 --- a/src/cpp/cpp_template_type.h +++ b/src/cpp/cpp_template_type.h @@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include -#include #include "cpp_template_parameter.h" diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index a6502391c3e..45d7c872759 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -15,23 +15,18 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #endif -#include -#include #include -#include -#include -#include #include -#include - #include +#include +#include + #include #include -#include "cpp_type2name.h" -#include "cpp_convert_type.h" #include "cpp_exception_id.h" +#include "cpp_type2name.h" #include "expr2cpp.h" bool cpp_typecheckt::find_parent( diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp index 565bca8a4bb..c4c85637878 100644 --- a/src/cpp/cpp_typecheck_initializer.cpp +++ b/src/cpp/cpp_typecheck_initializer.cpp @@ -14,12 +14,9 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include #include -#include #include -#include "cpp_util.h" - /// Initialize an object with a value void cpp_typecheckt::convert_initializer(symbolt &symbol) { diff --git a/src/goto-analyzer/static_show_domain.cpp b/src/goto-analyzer/static_show_domain.cpp index 99c8d63cefd..835311faf09 100644 --- a/src/goto-analyzer/static_show_domain.cpp +++ b/src/goto-analyzer/static_show_domain.cpp @@ -8,6 +8,8 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk #include "static_show_domain.h" +#include + #include /// Runs the analyzer and then prints out the domain diff --git a/src/goto-analyzer/static_show_domain.h b/src/goto-analyzer/static_show_domain.h index 1b2c3ee3772..71a6e90ef92 100644 --- a/src/goto-analyzer/static_show_domain.h +++ b/src/goto-analyzer/static_show_domain.h @@ -11,12 +11,10 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk #include -#include -#include - -#include - -#include +class ai_baset; +class goto_modelt; +class message_handlert; +class optionst; bool static_show_domain( const goto_modelt &, diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp index 9e6ffa57822..08e29037c70 100644 --- a/src/goto-analyzer/static_simplifier.cpp +++ b/src/goto-analyzer/static_simplifier.cpp @@ -6,17 +6,17 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk \*******************************************************************/ +#include "static_simplifier.h" + +#include +#include + +#include #include #include #include -#include -#include -#include -#include - -#include "static_simplifier.h" - +#include /// Simplifies the program using the information in the abstract domain. /// \param goto_model: the program analyzed diff --git a/src/goto-analyzer/static_simplifier.h b/src/goto-analyzer/static_simplifier.h index 59e741fba83..557d94737c0 100644 --- a/src/goto-analyzer/static_simplifier.h +++ b/src/goto-analyzer/static_simplifier.h @@ -11,12 +11,10 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk #include -#include -#include - -#include - -#include +class ai_baset; +class goto_modelt; +class message_handlert; +class optionst; bool static_simplifier( goto_modelt &, diff --git a/src/goto-analyzer/static_verifier.cpp b/src/goto-analyzer/static_verifier.cpp index 660d20bd37e..f4fbc6320b7 100644 --- a/src/goto-analyzer/static_verifier.cpp +++ b/src/goto-analyzer/static_verifier.cpp @@ -8,11 +8,14 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk #include "static_verifier.h" -#include -#include -#include #include +#include +#include +#include +#include + +#include /// Runs the analyzer and then prints out the domain /// \param goto_model: the program analyzed diff --git a/src/goto-analyzer/static_verifier.h b/src/goto-analyzer/static_verifier.h index e71bdfbb45c..87358a30958 100644 --- a/src/goto-analyzer/static_verifier.h +++ b/src/goto-analyzer/static_verifier.h @@ -11,12 +11,10 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk #include -#include -#include - -#include - -#include +class ai_baset; +class goto_modelt; +class message_handlert; +class optionst; bool static_verifier( const goto_modelt &, diff --git a/src/goto-analyzer/unreachable_instructions.cpp b/src/goto-analyzer/unreachable_instructions.cpp index 0e783baaba5..c691142aead 100644 --- a/src/goto-analyzer/unreachable_instructions.cpp +++ b/src/goto-analyzer/unreachable_instructions.cpp @@ -13,18 +13,16 @@ Date: April 2016 #include "unreachable_instructions.h" -#include - -#include -#include #include +#include +#include #include -#include - -#include #include +#include +#include + typedef std::map dead_mapt; static void unreachable_instructions( diff --git a/src/goto-analyzer/unreachable_instructions.h b/src/goto-analyzer/unreachable_instructions.h index edffd0f7b1c..eeee658ea52 100644 --- a/src/goto-analyzer/unreachable_instructions.h +++ b/src/goto-analyzer/unreachable_instructions.h @@ -14,14 +14,12 @@ Date: April 2016 #ifndef CPROVER_GOTO_ANALYZER_UNREACHABLE_INSTRUCTIONS_H #define CPROVER_GOTO_ANALYZER_UNREACHABLE_INSTRUCTIONS_H -#include - -#include - -#include -#include +#include +class ai_baset; class goto_modelt; +class message_handlert; +class optionst; void unreachable_instructions( const goto_modelt &, diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index c092f940f95..98550ce7375 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -15,27 +15,21 @@ Date: June 2006 #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 #include diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp index c7ede967768..d89900d11f3 100644 --- a/src/goto-cc/linker_script_merge.cpp +++ b/src/goto-cc/linker_script_merge.cpp @@ -6,32 +6,25 @@ Author: Kareem Khazem , 2017 \*******************************************************************/ -#include +#include "linker_script_merge.h" #include -#include -#include -#include #include +#include #include #include -#include -#include #include -#include #include -#include #include +#include + #include #include #include -#include "compile.h" -#include "linker_script_merge.h" - int linker_script_merget::add_linker_script_definitions() { if(!cmdline.isset('T') || elf_binaries.size()!=1) diff --git a/src/goto-diff/goto_diff.h b/src/goto-diff/goto_diff.h index 72171a76b31..efb90d1ed1d 100644 --- a/src/goto-diff/goto_diff.h +++ b/src/goto-diff/goto_diff.h @@ -12,13 +12,14 @@ Author: Peter Schrammel #ifndef CPROVER_GOTO_DIFF_GOTO_DIFF_H #define CPROVER_GOTO_DIFF_GOTO_DIFF_H -#include - -#include #include -#include +#include +#include +class goto_modelt; +class json_arrayt; +class json_objectt; class optionst; class goto_difft:public messaget diff --git a/src/goto-diff/goto_diff_base.cpp b/src/goto-diff/goto_diff_base.cpp index db3b925d702..a06b13edf2b 100644 --- a/src/goto-diff/goto_diff_base.cpp +++ b/src/goto-diff/goto_diff_base.cpp @@ -11,11 +11,12 @@ Author: Peter Schrammel #include "goto_diff.h" -#include - #include #include +#include +#include + /// Output diff result void goto_difft::output_functions() const { diff --git a/src/goto-diff/syntactic_diff.cpp b/src/goto-diff/syntactic_diff.cpp index 83f4ef04a78..558bf1a8eb8 100644 --- a/src/goto-diff/syntactic_diff.cpp +++ b/src/goto-diff/syntactic_diff.cpp @@ -11,6 +11,8 @@ Author: Peter Schrammel #include "syntactic_diff.h" +#include + bool syntactic_difft::operator()() { forall_goto_functions(it, goto_model1.goto_functions) diff --git a/src/goto-instrument/alignment_checks.cpp b/src/goto-instrument/alignment_checks.cpp index 68c173bda7a..758539c68be 100644 --- a/src/goto-instrument/alignment_checks.cpp +++ b/src/goto-instrument/alignment_checks.cpp @@ -11,9 +11,8 @@ Module: Alignment Checks #include "alignment_checks.h" -#include #include -#include +#include void print_struct_alignment_problems( const symbol_tablet &symbol_table, diff --git a/src/goto-instrument/call_sequences.cpp b/src/goto-instrument/call_sequences.cpp index 82da31087b8..ca36d43ee99 100644 --- a/src/goto-instrument/call_sequences.cpp +++ b/src/goto-instrument/call_sequences.cpp @@ -15,9 +15,7 @@ Date: April 2013 #include #include -#include -#include #include #include diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 16f3ebe8312..98d0d1248eb 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -13,7 +13,6 @@ Date: February 2016 #include "code_contracts.h" -#include #include #include diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index c51a6859d3e..2715f303063 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -11,16 +11,10 @@ Author: Daniel Kroening, kroening@kroening.com #include "dump_c.h" -#include -#include - +#include #include -#include -#include -#include #include -#include -#include +#include #include #include @@ -28,8 +22,8 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include "goto_program2code.h" #include "dump_c_class.h" +#include "goto_program2code.h" inline std::ostream &operator << (std::ostream &out, dump_ct &src) { diff --git a/src/goto-instrument/mmio.cpp b/src/goto-instrument/mmio.cpp index db9df4293fe..0e0a2a03693 100644 --- a/src/goto-instrument/mmio.cpp +++ b/src/goto-instrument/mmio.cpp @@ -15,18 +15,6 @@ Date: September 2011 #include -#include -#include - -#if 0 -#include -#include -#include - -#include -#endif - -#include "interrupt.h" #include "rw_set.h" #ifdef LOCAL_MAY diff --git a/src/goto-instrument/nondet_static.cpp b/src/goto-instrument/nondet_static.cpp index 2dce04f9d22..51cbf5034fe 100644 --- a/src/goto-instrument/nondet_static.cpp +++ b/src/goto-instrument/nondet_static.cpp @@ -14,13 +14,7 @@ Date: November 2011 #include "nondet_static.h" -#include -#include -#include -#include - #include -#include #include diff --git a/src/goto-instrument/object_id.h b/src/goto-instrument/object_id.h index 98e4b03033b..509bf6a15c5 100644 --- a/src/goto-instrument/object_id.h +++ b/src/goto-instrument/object_id.h @@ -12,8 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_INSTRUMENT_OBJECT_ID_H #define CPROVER_GOTO_INSTRUMENT_OBJECT_ID_H -#include #include +#include #include #include diff --git a/src/goto-instrument/race_check.cpp b/src/goto-instrument/race_check.cpp index 8517e90f1ae..0289148f1ec 100644 --- a/src/goto-instrument/race_check.cpp +++ b/src/goto-instrument/race_check.cpp @@ -13,16 +13,6 @@ Date: February 2006 #include "race_check.h" -#include -#include -#include -#include -#include - -#include -#include - -#include #include #include diff --git a/src/goto-instrument/rw_set.h b/src/goto-instrument/rw_set.h index 69072389347..3dd99a9a7db 100644 --- a/src/goto-instrument/rw_set.h +++ b/src/goto-instrument/rw_set.h @@ -19,17 +19,17 @@ Date: February 2006 #include #include -#include -#include #include #include -#include #ifdef LOCAL_MAY #include #endif +class namespacet; +class value_setst; + // a container for read/write sets class rw_set_baset diff --git a/src/goto-instrument/stack_depth.cpp b/src/goto-instrument/stack_depth.cpp index a0e0457fa24..9784d648f39 100644 --- a/src/goto-instrument/stack_depth.cpp +++ b/src/goto-instrument/stack_depth.cpp @@ -13,12 +13,7 @@ Date: November 2011 #include "stack_depth.h" -#include -#include -#include -#include #include -#include #include diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp index 9611f56d2f7..6d130be954b 100644 --- a/src/goto-instrument/wmm/goto2graph.cpp +++ b/src/goto-instrument/wmm/goto2graph.cpp @@ -16,17 +16,8 @@ Date: 2012 #include #include #include -#include -#ifndef _WIN32 -#include -#endif - -#include -#include #include -#include -#include #include diff --git a/src/goto-instrument/wmm/shared_buffers.cpp b/src/goto-instrument/wmm/shared_buffers.cpp index 4f8a5e65247..feadf6af1ad 100644 --- a/src/goto-instrument/wmm/shared_buffers.cpp +++ b/src/goto-instrument/wmm/shared_buffers.cpp @@ -8,12 +8,12 @@ Author: Daniel Kroening, kroening@kroening.com #include "shared_buffers.h" +#include + #include -#include "fence.h" #include "../rw_set.h" - -#include +#include "fence.h" /// returns a unique id (for fresh variables) std::string shared_bufferst::unique(void) diff --git a/src/goto-instrument/wmm/weak_memory.cpp b/src/goto-instrument/wmm/weak_memory.cpp index 1f2e38b61da..155e2064383 100644 --- a/src/goto-instrument/wmm/weak_memory.cpp +++ b/src/goto-instrument/wmm/weak_memory.cpp @@ -23,10 +23,6 @@ Date: September 2011 #include -#include -#include -#include - #include #include diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index ba1dfb7c685..13685785d71 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -17,17 +17,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include -#include #include #include -#include -#include -#include -#include -#include -#include -#include #include diff --git a/src/goto-programs/class_hierarchy.h b/src/goto-programs/class_hierarchy.h index 9b926d25e18..1d180369765 100644 --- a/src/goto-programs/class_hierarchy.h +++ b/src/goto-programs/class_hierarchy.h @@ -19,7 +19,9 @@ Date: April 2016 #include #include -#include +#include + +class symbol_tablet; class class_hierarchyt { diff --git a/src/goto-programs/generate_function_bodies.cpp b/src/goto-programs/generate_function_bodies.cpp index 64d12ce0d4a..aca0ed19aba 100644 --- a/src/goto-programs/generate_function_bodies.cpp +++ b/src/goto-programs/generate_function_bodies.cpp @@ -8,17 +8,10 @@ Author: Diffblue Ltd. #include "generate_function_bodies.h" -#include -#include -#include -#include - +#include #include #include -#include #include -#include -#include void generate_function_bodiest::generate_function_body( goto_functiont &function, diff --git a/src/goto-programs/goto_functions.h b/src/goto-programs/goto_functions.h index 12b6b8c98be..0289fbdfcc2 100644 --- a/src/goto-programs/goto_functions.h +++ b/src/goto-programs/goto_functions.h @@ -14,14 +14,12 @@ Date: June 2003 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_H #define CPROVER_GOTO_PROGRAMS_GOTO_FUNCTIONS_H -#include "goto_program.h" - -#include -#include +#include -#include -#include #include +#include + +#include "goto_program.h" class goto_functiont { diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index aa53dfd97d8..88c84258b2f 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H #define CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H -#include #include #include #include diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp index 15db12bde80..517f66f050b 100644 --- a/src/goto-programs/interpreter_evaluate.cpp +++ b/src/goto-programs/interpreter_evaluate.cpp @@ -11,16 +11,10 @@ Author: Daniel Kroening, kroening@kroening.com #include "interpreter_class.h" -#include -#include -#include - -#include -#include #include -#include -#include +#include #include +#include #include diff --git a/src/goto-programs/remove_asm.cpp b/src/goto-programs/remove_asm.cpp index d93032a33aa..8df9d6429e8 100644 --- a/src/goto-programs/remove_asm.cpp +++ b/src/goto-programs/remove_asm.cpp @@ -14,14 +14,13 @@ Date: December 2014 #include "remove_asm.h" -#include - #include -#include #include #include +#include "goto_model.h" + class remove_asmt { public: diff --git a/src/goto-programs/remove_asm.h b/src/goto-programs/remove_asm.h index 913fe85c336..49d668c74d9 100644 --- a/src/goto-programs/remove_asm.h +++ b/src/goto-programs/remove_asm.h @@ -15,7 +15,10 @@ Date: December 2014 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_ASM_H #define CPROVER_GOTO_PROGRAMS_REMOVE_ASM_H -#include +#include + +class goto_modelt; +class symbol_tablet; void remove_asm( goto_functionst::goto_functiont &goto_function, diff --git a/src/goto-programs/remove_calls_no_body.cpp b/src/goto-programs/remove_calls_no_body.cpp index b8e46c41edf..62121dcfe17 100644 --- a/src/goto-programs/remove_calls_no_body.cpp +++ b/src/goto-programs/remove_calls_no_body.cpp @@ -9,9 +9,12 @@ Author: Daniel Poetzl /// \file /// Remove calls to functions without a body -#include #include "remove_calls_no_body.h" +#include + +#include "goto_functions.h" + /// Remove a single call /// \param goto_program: goto program to modify /// \param target: iterator pointing to the call diff --git a/src/goto-programs/remove_calls_no_body.h b/src/goto-programs/remove_calls_no_body.h index de10c426f2e..9b7382328ce 100644 --- a/src/goto-programs/remove_calls_no_body.h +++ b/src/goto-programs/remove_calls_no_body.h @@ -12,7 +12,9 @@ Author: Daniel Poetzl #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_CALLS_NO_BODY_H #define CPROVER_GOTO_PROGRAMS_REMOVE_CALLS_NO_BODY_H -#include "goto_functions.h" +#include "goto_program.h" + +class goto_functionst; class remove_calls_no_bodyt { diff --git a/src/goto-programs/remove_complex.cpp b/src/goto-programs/remove_complex.cpp index 141fc4709fc..ef5b351f54d 100644 --- a/src/goto-programs/remove_complex.cpp +++ b/src/goto-programs/remove_complex.cpp @@ -14,6 +14,10 @@ Date: September 2014 #include "remove_complex.h" #include +#include +#include + +#include "goto_model.h" static exprt complex_member(const exprt &expr, irep_idt id) { diff --git a/src/goto-programs/remove_complex.h b/src/goto-programs/remove_complex.h index 098470ecc1a..c448f4a15e7 100644 --- a/src/goto-programs/remove_complex.h +++ b/src/goto-programs/remove_complex.h @@ -14,7 +14,9 @@ Date: September 2014 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_COMPLEX_H #define CPROVER_GOTO_PROGRAMS_REMOVE_COMPLEX_H -#include +class goto_functionst; +class goto_modelt; +class symbol_tablet; void remove_complex(symbol_tablet &, goto_functionst &); diff --git a/src/goto-programs/remove_const_function_pointers.cpp b/src/goto-programs/remove_const_function_pointers.cpp index 9b8e67c8b68..81e2812136b 100644 --- a/src/goto-programs/remove_const_function_pointers.cpp +++ b/src/goto-programs/remove_const_function_pointers.cpp @@ -11,9 +11,14 @@ Author: Thomas Kiley, thomas.kiley@diffblue.com #include "remove_const_function_pointers.h" -#include -#include #include +#include +#include +#include + +#include + +#include "goto_functions.h" #define LOG(message, irep) \ debug() << "Case " << __LINE__ << " : " << message << "\n" \ diff --git a/src/goto-programs/remove_const_function_pointers.h b/src/goto-programs/remove_const_function_pointers.h index 469deaec032..0299de8b383 100644 --- a/src/goto-programs/remove_const_function_pointers.h +++ b/src/goto-programs/remove_const_function_pointers.h @@ -12,13 +12,22 @@ Author: Thomas Kiley, thomas.kiley@diffblue.com #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_CONST_FUNCTION_POINTERS_H #define CPROVER_GOTO_PROGRAMS_REMOVE_CONST_FUNCTION_POINTERS_H +#include #include -#include "goto_model.h" -#include #include -#include - +#include +#include + +class address_of_exprt; +class dereference_exprt; +class index_exprt; +class member_exprt; +class namespacet; +class struct_exprt; +class symbol_exprt; +class symbol_tablet; +class typecast_exprt; class remove_const_function_pointerst:public messaget { diff --git a/src/goto-programs/remove_function_pointers.h b/src/goto-programs/remove_function_pointers.h index 3038a940637..4a7bbfb09b5 100644 --- a/src/goto-programs/remove_function_pointers.h +++ b/src/goto-programs/remove_function_pointers.h @@ -14,8 +14,11 @@ Date: June 2003 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_FUNCTION_POINTERS_H #define CPROVER_GOTO_PROGRAMS_REMOVE_FUNCTION_POINTERS_H -#include "goto_model.h" -#include +class goto_functionst; +class goto_programt; +class goto_modelt; +class message_handlert; +class symbol_tablet; // remove indirect function calls // and replace by case-split diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp index 4c275ff9bbb..5257c83ea0a 100644 --- a/src/goto-programs/remove_returns.cpp +++ b/src/goto-programs/remove_returns.cpp @@ -14,7 +14,8 @@ Date: September 2009 #include "remove_returns.h" #include -#include + +#include "goto_model.h" class remove_returnst { diff --git a/src/goto-programs/remove_returns.h b/src/goto-programs/remove_returns.h index f2017111478..32d2a81c824 100644 --- a/src/goto-programs/remove_returns.h +++ b/src/goto-programs/remove_returns.h @@ -14,10 +14,17 @@ Date: September 2009 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H #define CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H -#include +#include + +#include #define RETURN_VALUE_SUFFIX "#return_value" +class goto_functionst; +class goto_model_functiont; +class goto_modelt; +class symbol_table_baset; + // Turns 'return x' into an assignment to fkt#return_value, // unless the function returns void, // and a 'goto the_end_of_the_function'. diff --git a/src/goto-programs/remove_skip.h b/src/goto-programs/remove_skip.h index 68f9a833994..6ff55bf3e03 100644 --- a/src/goto-programs/remove_skip.h +++ b/src/goto-programs/remove_skip.h @@ -12,8 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_SKIP_H #define CPROVER_GOTO_PROGRAMS_REMOVE_SKIP_H -#include "goto_functions.h" +#include "goto_program.h" +class goto_functionst; class goto_modelt; bool is_skip(const goto_programt &, goto_programt::const_targett); diff --git a/src/goto-programs/remove_unreachable.cpp b/src/goto-programs/remove_unreachable.cpp index 562546f377b..07d71adf471 100644 --- a/src/goto-programs/remove_unreachable.cpp +++ b/src/goto-programs/remove_unreachable.cpp @@ -14,6 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "goto_functions.h" + /// remove unreachable code void remove_unreachable(goto_programt &goto_program) { diff --git a/src/goto-programs/remove_unreachable.h b/src/goto-programs/remove_unreachable.h index 5267529d364..ec8ac9bb9fb 100644 --- a/src/goto-programs/remove_unreachable.h +++ b/src/goto-programs/remove_unreachable.h @@ -12,7 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_UNREACHABLE_H #define CPROVER_GOTO_PROGRAMS_REMOVE_UNREACHABLE_H -#include "goto_functions.h" +class goto_functionst; +class goto_programt; void remove_unreachable(goto_programt &goto_program); void remove_unreachable(goto_functionst &goto_functions); diff --git a/src/goto-programs/remove_unused_functions.cpp b/src/goto-programs/remove_unused_functions.cpp index 3092e114796..edb4c712ec2 100644 --- a/src/goto-programs/remove_unused_functions.cpp +++ b/src/goto-programs/remove_unused_functions.cpp @@ -13,6 +13,8 @@ Author: CM Wintersteiger #include +#include "goto_model.h" + void remove_unused_functions( goto_modelt &goto_model, message_handlert &message_handler) diff --git a/src/goto-programs/remove_unused_functions.h b/src/goto-programs/remove_unused_functions.h index 8c8b1739a98..d7fd2569e18 100644 --- a/src/goto-programs/remove_unused_functions.h +++ b/src/goto-programs/remove_unused_functions.h @@ -12,9 +12,14 @@ Author: CM Wintersteiger #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_UNUSED_FUNCTIONS_H #define CPROVER_GOTO_PROGRAMS_REMOVE_UNUSED_FUNCTIONS_H -#include +#include -#include +#include + +class goto_functionst; +class goto_modelt; +class message_handlert; +class symbol_tablet; void remove_unused_functions( goto_functionst &, diff --git a/src/goto-programs/remove_vector.cpp b/src/goto-programs/remove_vector.cpp index f2e7f5b9fe4..cabd5100698 100644 --- a/src/goto-programs/remove_vector.cpp +++ b/src/goto-programs/remove_vector.cpp @@ -14,6 +14,10 @@ Date: September 2014 #include "remove_vector.h" #include +#include +#include + +#include "goto_model.h" static bool have_to_remove_vector(const typet &type); diff --git a/src/goto-programs/remove_vector.h b/src/goto-programs/remove_vector.h index 960d75953a8..2bd1f623e95 100644 --- a/src/goto-programs/remove_vector.h +++ b/src/goto-programs/remove_vector.h @@ -14,7 +14,9 @@ Date: September 2014 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_VECTOR_H #define CPROVER_GOTO_PROGRAMS_REMOVE_VECTOR_H -#include +class goto_functionst; +class goto_modelt; +class symbol_tablet; void remove_vector(symbol_tablet &, goto_functionst &); diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index 86e19e7de81..a242577e8cd 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -8,18 +8,16 @@ Author: Daniel Kroening, kroening@kroening.com /// \file /// Remove Virtual Function (Method) Calls -#include - #include "remove_virtual_functions.h" -#include "class_hierarchy.h" -#include "class_identifier.h" -#include +#include -#include -#include #include +#include "class_identifier.h" +#include "goto_model.h" +#include "resolve_inherited_component.h" + class remove_virtual_functionst { public: diff --git a/src/goto-programs/remove_virtual_functions.h b/src/goto-programs/remove_virtual_functions.h index 43bd0f2fea8..ae5d257f6fd 100644 --- a/src/goto-programs/remove_virtual_functions.h +++ b/src/goto-programs/remove_virtual_functions.h @@ -14,8 +14,15 @@ Date: April 2016 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_VIRTUAL_FUNCTIONS_H #define CPROVER_GOTO_PROGRAMS_REMOVE_VIRTUAL_FUNCTIONS_H -#include "goto_model.h" +#include + #include "class_hierarchy.h" +#include "goto_program.h" + +class goto_functionst; +class goto_model_functiont; +class goto_modelt; +class symbol_table_baset; // remove virtual function calls // and replace by case-split diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp index fd5a123c6df..5a9043cff2b 100644 --- a/src/goto-programs/string_abstraction.cpp +++ b/src/goto-programs/string_abstraction.cpp @@ -16,14 +16,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include -#include -#include -#include #include -#include - #include "pointer_arithmetic.h" bool string_abstractiont::build_wrap( diff --git a/src/goto-programs/vcd_goto_trace.cpp b/src/goto-programs/vcd_goto_trace.cpp index 7acc15e890b..9e736033df1 100644 --- a/src/goto-programs/vcd_goto_trace.cpp +++ b/src/goto-programs/vcd_goto_trace.cpp @@ -13,13 +13,11 @@ Date: June 2011 #include "vcd_goto_trace.h" -#include -#include #include +#include -#include -#include #include +#include std::string as_vcd_binary( const exprt &expr, diff --git a/src/goto-symex/equation_conversion_exceptions.h b/src/goto-symex/equation_conversion_exceptions.h index f2055c1c9ec..ffa57abefe0 100644 --- a/src/goto-symex/equation_conversion_exceptions.h +++ b/src/goto-symex/equation_conversion_exceptions.h @@ -12,7 +12,7 @@ Author: Diffblue Ltd. #ifndef CPROVER_GOTO_SYMEX_EQUATION_CONVERSION_EXCEPTIONS_H #define CPROVER_GOTO_SYMEX_EQUATION_CONVERSION_EXCEPTIONS_H -#include +#include #include diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 7d7edb8891f..117693b8391 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -14,13 +14,13 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include "goto_symex_state.h" #include "symex_target_equation.h" +class byte_extract_exprt; class typet; class code_typet; class symbol_tablet; diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index 6294e47b3a1..f827f1ecaea 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -11,25 +11,15 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_symex.h" -#include -#include #include -#include -#include +#include +#include #include -#include -#include -#include #include -#include #include -#include -#include #include -#include "goto_symex_state.h" - inline static typet c_sizeof_type_rec(const exprt &expr) { const irept &sizeof_type=expr.find(ID_C_c_sizeof_type); diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp index 5e1e0cf4c91..ce6265e1c20 100644 --- a/src/goto-symex/symex_clean_expr.cpp +++ b/src/goto-symex/symex_clean_expr.cpp @@ -12,11 +12,10 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_symex.h" #include -#include -#include #include -#include +#include #include +#include /// Given an expression, find the root object and the offset into it. /// diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp index 95b8866865e..e259a515489 100644 --- a/src/goto-symex/symex_dereference.cpp +++ b/src/goto-symex/symex_dereference.cpp @@ -11,16 +11,14 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_symex.h" -#include -#include #include #include #include +#include +#include +#include #include -#include - -#include #include "symex_dereference_state.h" diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index 37e173928c4..6de8995364d 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -11,19 +11,11 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_symex.h" -#include - -#include -#include -#include #include #include -#include -#include - +#include #include - -#include +#include bool goto_symext::get_unwind_recursion( const irep_idt &identifier, diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp index f3cc50c32bb..30ca539f429 100644 --- a/src/goto-symex/symex_other.cpp +++ b/src/goto-symex/symex_other.cpp @@ -12,14 +12,10 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_symex.h" #include -#include -#include #include -#include -#include #include -#include #include +#include void goto_symext::havoc_rec( statet &state, diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index ef4a4e70cc8..2556ee4d7e9 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -8,31 +8,15 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_entry_point.h" -#include -#include -#include -#include - -#include - -#include -#include #include -#include -#include -#include -#include -#include -#include -#include -#include #include #include +#include + #include #include "java_object_factory.h" -#include "java_types.h" #include "java_utils.h" static void create_initialize(symbol_table_baset &symbol_table) diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index feaeb218f6c..612a66f9ce5 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -8,32 +8,14 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_object_factory.h" -#include -#include - -#include #include -#include -#include -#include -#include #include -#include #include -#include -#include - -#include #include -#include - -#include "java_types.h" -#include "java_utils.h" -#include "java_string_library_preprocess.h" -#include "java_root_class.h" #include "generic_parameter_specialization_map_keys.h" +#include "java_root_class.h" class java_object_factoryt { diff --git a/src/jsil/jsil_entry_point.cpp b/src/jsil/jsil_entry_point.cpp index a8f1278e961..43f60bd1950 100644 --- a/src/jsil/jsil_entry_point.cpp +++ b/src/jsil/jsil_entry_point.cpp @@ -13,10 +13,7 @@ Author: Michael Tautschnig, tautschn@amazon.com #include #include -#include #include -#include -#include #include diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp index 5b5a1d36fd2..a93e0919e64 100644 --- a/src/linking/linking.cpp +++ b/src/linking/linking.cpp @@ -12,15 +12,13 @@ Author: Daniel Kroening, kroening@kroening.com #include "linking.h" #include -#include +#include +#include -#include -#include #include -#include -#include -#include +#include #include +#include #include diff --git a/src/linking/remove_internal_symbols.cpp b/src/linking/remove_internal_symbols.cpp index 91f6e3c411d..d563278ff52 100644 --- a/src/linking/remove_internal_symbols.cpp +++ b/src/linking/remove_internal_symbols.cpp @@ -11,12 +11,11 @@ Author: Daniel Kroening #include "remove_internal_symbols.h" -#include -#include +#include #include +#include #include -#include -#include +#include #include "static_lifetime_init.h" diff --git a/src/linking/static_lifetime_init.h b/src/linking/static_lifetime_init.h index 0955fc1f57c..829e2e16a05 100644 --- a/src/linking/static_lifetime_init.h +++ b/src/linking/static_lifetime_init.h @@ -10,11 +10,12 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_LINKING_STATIC_LIFETIME_INIT_H #define CPROVER_LINKING_STATIC_LIFETIME_INIT_H -#include -#include -#include #include +class message_handlert; +class source_locationt; +class symbol_tablet; + bool static_lifetime_init( symbol_tablet &symbol_table, const source_locationt &source_location, diff --git a/src/linking/zero_initializer.cpp b/src/linking/zero_initializer.cpp index 0916256ab5d..675cdb7dd7f 100644 --- a/src/linking/zero_initializer.cpp +++ b/src/linking/zero_initializer.cpp @@ -11,16 +11,13 @@ Author: Daniel Kroening, kroening@kroening.com #include "zero_initializer.h" -#include - -#include -#include #include -#include -#include +#include +#include +#include #include +#include -#include #include class zero_initializert:public messaget diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index 0e528f5760b..7cd08339d7a 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -14,17 +14,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include -#include -#include -#include -#include -#include #include -#include -#include - +#include #include +#include +#include #include diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index 4e437ede5ea..3e6e653d7a7 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -16,35 +16,23 @@ Author: Daniel Kroening, kroening@kroening.com #include #endif -#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 #include -#include #include -#include - -#include "pointer_offset_sum.h" - // global data, horrible unsigned int value_set_dereferencet::invalid_counter=0; diff --git a/src/solvers/flattening/boolbv_update.cpp b/src/solvers/flattening/boolbv_update.cpp index f5121f8bf91..668b8cc8fdc 100644 --- a/src/solvers/flattening/boolbv_update.cpp +++ b/src/solvers/flattening/boolbv_update.cpp @@ -8,13 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "boolbv.h" -#include -#include #include -#include -#include - -#include bvt boolbvt::convert_update(const exprt &expr) { diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index b82a54ac615..7043938eccf 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -8,14 +8,10 @@ Author: Daniel Kroening, kroening@kroening.com #include "bv_pointers.h" +#include #include #include -#include -#include -#include -#include #include -#include literalt bv_pointerst::convert_rest(const exprt &expr) { diff --git a/src/solvers/flattening/flatten_byte_operators.cpp b/src/solvers/flattening/flatten_byte_operators.cpp index 42054cc61dc..2cc586c7c02 100644 --- a/src/solvers/flattening/flatten_byte_operators.cpp +++ b/src/solvers/flattening/flatten_byte_operators.cpp @@ -6,19 +6,17 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include -#include -#include -#include +#include "flatten_byte_operators.h" + #include -#include #include +#include #include +#include #include #include #include "flatten_byte_extract_exceptions.h" -#include "flatten_byte_operators.h" /// rewrite an object into its individual bytes /// \par parameters: src object to unpack diff --git a/src/solvers/flattening/pointer_logic.cpp b/src/solvers/flattening/pointer_logic.cpp index 5bbbad458f2..d0a2a866903 100644 --- a/src/solvers/flattening/pointer_logic.cpp +++ b/src/solvers/flattening/pointer_logic.cpp @@ -15,9 +15,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include -#include +#include #include +#include +#include bool pointer_logict::is_dynamic_object(const exprt &expr) const { diff --git a/src/util/base_type.cpp b/src/util/base_type.cpp index 4aba15b5505..d32a2836aaf 100644 --- a/src/util/base_type.cpp +++ b/src/util/base_type.cpp @@ -11,11 +11,10 @@ Author: Daniel Kroening, kroening@kroening.com #include "base_type.h" -#include #include -#include "std_types.h" #include "namespace.h" +#include "std_types.h" #include "symbol.h" #include "union_find.h" diff --git a/src/util/fresh_symbol.cpp b/src/util/fresh_symbol.cpp index 0f7c3a9daf2..c77c7e33e47 100644 --- a/src/util/fresh_symbol.cpp +++ b/src/util/fresh_symbol.cpp @@ -13,6 +13,8 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include "namespace.h" #include "rename.h" +#include "symbol.h" +#include "symbol_table_base.h" /// Installs a fresh-named symbol with the requested name pattern /// \par parameters: `type`: type of new symbol diff --git a/src/util/fresh_symbol.h b/src/util/fresh_symbol.h index 8cdedc56977..0d1601ad180 100644 --- a/src/util/fresh_symbol.h +++ b/src/util/fresh_symbol.h @@ -14,10 +14,12 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include -#include -#include -#include -#include +#include "irep.h" + +class source_locationt; +class symbolt; +class symbol_table_baset; +class typet; symbolt &get_fresh_aux_symbol( const typet &type, diff --git a/src/util/graph.h b/src/util/graph.h index 85ad33c448d..6b7fd6e07f7 100644 --- a/src/util/graph.h +++ b/src/util/graph.h @@ -12,15 +12,15 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_GRAPH_H #define CPROVER_UTIL_GRAPH_H +#include +#include +#include +#include #include -#include #include -#include -#include -#include -#include #include -#include +#include +#include #include "invariant.h" diff --git a/src/util/invariant_utils.h b/src/util/invariant_utils.h index d448fedfeb3..3dd9d386418 100644 --- a/src/util/invariant_utils.h +++ b/src/util/invariant_utils.h @@ -10,8 +10,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com #define CPROVER_UTIL_INVARIANT_TYPES_H #include "invariant.h" - -#include +#include "irep.h" #include diff --git a/src/util/irep.h b/src/util/irep.h index fbaf0ad5a94..2365989bfaa 100644 --- a/src/util/irep.h +++ b/src/util/irep.h @@ -12,8 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include -#include #include "irep_ids.h" diff --git a/src/util/irep_hash_container.h b/src/util/irep_hash_container.h index 382130659e0..65342ba99b1 100644 --- a/src/util/irep_hash_container.h +++ b/src/util/irep_hash_container.h @@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_IREP_HASH_CONTAINER_H #define CPROVER_UTIL_IREP_HASH_CONTAINER_H -#include // for size_t #include #include "numbering.h" @@ -22,7 +21,7 @@ class irept; class irep_hash_container_baset { public: - size_t number(const irept &irep); + std::size_t number(const irept &irep); explicit irep_hash_container_baset(bool _full):full(_full) { @@ -41,23 +40,23 @@ class irep_hash_container_baset struct pointer_hasht { - size_t operator()(const void *p) const + std::size_t operator()(const void *p) const { - return (size_t)p; + return (std::size_t)p; } }; - typedef std::unordered_map + typedef std::unordered_map ptr_hasht; ptr_hasht ptr_hash; // this is the second level: content - typedef std::vector packedt; + typedef std::vector packedt; struct vector_hasht { - size_t operator()(const packedt &p) const; + std::size_t operator()(const packedt &p) const; }; typedef hash_numbering numberingt; diff --git a/src/util/json_irep.h b/src/util/json_irep.h index 6fdc3dfc92d..6e6fe6b1a55 100644 --- a/src/util/json_irep.h +++ b/src/util/json_irep.h @@ -12,7 +12,7 @@ Author: Thomas Kiley, thomas.kiley@diffblue.com #ifndef CPROVER_UTIL_JSON_IREP_H #define CPROVER_UTIL_JSON_IREP_H -#include +#include "irep.h" class jsont; class json_objectt; diff --git a/src/util/json_stream.h b/src/util/json_stream.h index f27e360c9a3..cbb4689a5de 100644 --- a/src/util/json_stream.h +++ b/src/util/json_stream.h @@ -9,8 +9,8 @@ Author: Peter Schrammel #ifndef CPROVER_UTIL_JSON_STREAM_H #define CPROVER_UTIL_JSON_STREAM_H -#include #include +#include #include "json.h" #include "invariant.h" diff --git a/src/util/nondet_bool.h b/src/util/nondet_bool.h index af628d3456e..700b85ec5b0 100644 --- a/src/util/nondet_bool.h +++ b/src/util/nondet_bool.h @@ -12,8 +12,8 @@ Author: Chris Smowton, chris@smowton.net #ifndef CPROVER_UTIL_NONDET_BOOL_H #define CPROVER_UTIL_NONDET_BOOL_H -#include -#include +#include "std_expr.h" +#include "std_types.h" /// \par parameters: Desired type (C_bool or plain bool) /// \return nondet expr of that type diff --git a/src/util/nondet_ifthenelse.h b/src/util/nondet_ifthenelse.h index 664a6bdf1b2..cf1966526ef 100644 --- a/src/util/nondet_ifthenelse.h +++ b/src/util/nondet_ifthenelse.h @@ -12,7 +12,7 @@ Author: Chris Smowton, chris@smowton.net #ifndef CPROVER_UTIL_NONDET_IFTHENELSE_H #define CPROVER_UTIL_NONDET_IFTHENELSE_H -#include +#include "std_code.h" class symbol_tablet; class source_locationt; diff --git a/src/util/numbering.h b/src/util/numbering.h index f932874695a..42e18354e21 100644 --- a/src/util/numbering.h +++ b/src/util/numbering.h @@ -9,13 +9,12 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_NUMBERING_H #define CPROVER_UTIL_NUMBERING_H -#include #include #include #include -#include -#include +#include "invariant.h" +#include "optional.h" /// \tparam Map a map from a key type to some numeric type template diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp index 21dbdbb23f7..2e315ba242f 100644 --- a/src/util/pointer_offset_size.cpp +++ b/src/util/pointer_offset_size.cpp @@ -11,17 +11,13 @@ Author: Daniel Kroening, kroening@kroening.com #include "pointer_offset_size.h" +#include "arith_tools.h" #include "c_types.h" -#include "expr.h" #include "invariant.h" -#include "arith_tools.h" -#include "std_types.h" -#include "std_expr.h" -#include "expr_util.h" -#include "simplify_expr.h" #include "namespace.h" -#include "symbol.h" +#include "simplify_expr.h" #include "ssa_expr.h" +#include "std_expr.h" member_offset_iterator::member_offset_iterator( const struct_typet &_type, diff --git a/src/util/pointer_predicates.cpp b/src/util/pointer_predicates.cpp index 312166f0088..966ebdae021 100644 --- a/src/util/pointer_predicates.cpp +++ b/src/util/pointer_predicates.cpp @@ -11,14 +11,12 @@ Author: Daniel Kroening, kroening@kroening.com #include "pointer_predicates.h" +#include "arith_tools.h" #include "c_types.h" #include "cprover_prefix.h" #include "namespace.h" -#include "std_expr.h" -#include "expr_util.h" -#include "arith_tools.h" #include "pointer_offset_size.h" -#include "config.h" +#include "std_expr.h" #include "symbol.h" exprt pointer_object(const exprt &p) diff --git a/src/util/rational.h b/src/util/rational.h index 809f237c95a..a043ed0923d 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -10,9 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_RATIONAL_H #define CPROVER_UTIL_RATIONAL_H -#include -#include - #include "mp_arith.h" class constant_exprt; diff --git a/src/util/refined_string_type.cpp b/src/util/refined_string_type.cpp index 818eb9e4391..91cbc7ff090 100644 --- a/src/util/refined_string_type.cpp +++ b/src/util/refined_string_type.cpp @@ -18,6 +18,8 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include "refined_string_type.h" +#include "std_expr.h" + refined_string_typet::refined_string_typet( const typet &index_type, const typet &char_type) { diff --git a/src/util/refined_string_type.h b/src/util/refined_string_type.h index ecef73288ea..bc597556b2d 100644 --- a/src/util/refined_string_type.h +++ b/src/util/refined_string_type.h @@ -19,11 +19,8 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #ifndef CPROVER_UTIL_REFINED_STRING_TYPE_H #define CPROVER_UTIL_REFINED_STRING_TYPE_H -#include -#include -#include -#include -#include +#include "cprover_prefix.h" +#include "std_types.h" // Internal type used for string refinement class refined_string_typet: public struct_typet diff --git a/src/util/sharing_map.h b/src/util/sharing_map.h index a558ec42901..1c8943ae1ac 100644 --- a/src/util/sharing_map.h +++ b/src/util/sharing_map.h @@ -15,17 +15,15 @@ Author: Daniel Poetzl #include #include #include -#include #include #include #include #include #include -#include -#include -#include -#include +#include "irep.h" +#include "sharing_node.h" +#include "threeval.h" #define _sm_assert(b) assert(b) //#define _sm_assert(b) diff --git a/src/util/sharing_node.h b/src/util/sharing_node.h index 9cec1cd2f3a..2ecebabb467 100644 --- a/src/util/sharing_node.h +++ b/src/util/sharing_node.h @@ -15,7 +15,6 @@ Author: Daniel Poetzl #include #include #include -#include #include "invariant.h" diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 4a0e2855d29..c2e07be9630 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -11,29 +11,21 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include "c_types.h" -#include "rational.h" -#include "simplify_expr_class.h" -#include "mp_arith.h" #include "arith_tools.h" -#include "replace_expr.h" -#include "std_types.h" +#include "base_type.h" +#include "byte_operators.h" +#include "c_types.h" +#include "config.h" +#include "endianness_map.h" #include "expr_util.h" -#include "std_expr.h" #include "fixedbv.h" +#include "namespace.h" #include "pointer_offset_size.h" +#include "rational.h" #include "rational_tools.h" -#include "config.h" -#include "base_type.h" -#include "type_eq.h" -#include "namespace.h" -#include "threeval.h" -#include "pointer_predicates.h" -#include "prefix.h" -#include "byte_operators.h" -#include "bv_arithmetic.h" -#include "endianness_map.h" #include "simplify_utils.h" +#include "std_expr.h" +#include "type_eq.h" // #define DEBUGX @@ -41,6 +33,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #endif +#include "simplify_expr_class.h" + // #define USE_CACHE #ifdef USE_CACHE diff --git a/src/util/simplify_expr_array.cpp b/src/util/simplify_expr_array.cpp index 026cb84105f..db64a51b243 100644 --- a/src/util/simplify_expr_array.cpp +++ b/src/util/simplify_expr_array.cpp @@ -8,14 +8,11 @@ Author: Daniel Kroening, kroening@kroening.com #include "simplify_expr_class.h" -#include - -#include "expr.h" -#include "namespace.h" -#include "std_expr.h" -#include "replace_expr.h" #include "arith_tools.h" +#include "namespace.h" #include "pointer_offset_size.h" +#include "replace_expr.h" +#include "std_expr.h" bool simplify_exprt::simplify_index(exprt &expr) { diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index c225997d2c8..da3c03da448 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -14,7 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "base_type.h" #include "bv_arithmetic.h" #include "config.h" -#include "expr.h" #include "expr_util.h" #include "fixedbv.h" #include "ieee_float.h" @@ -24,7 +23,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "rational.h" #include "rational_tools.h" #include "std_expr.h" -#include "string2int.h" bool simplify_exprt::simplify_bswap(bswap_exprt &expr) { diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index a1e26187897..fff9ba57f52 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -10,17 +10,15 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include "c_types.h" -#include "expr.h" -#include "namespace.h" -#include "std_expr.h" -#include "pointer_offset_size.h" #include "arith_tools.h" +#include "c_types.h" #include "config.h" #include "expr_util.h" -#include "threeval.h" -#include "prefix.h" +#include "namespace.h" +#include "pointer_offset_size.h" #include "pointer_predicates.h" +#include "std_expr.h" +#include "threeval.h" static bool is_dereference_integer_object( const exprt &expr, diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp index e6195f2cb54..331d04c3001 100644 --- a/src/util/simplify_expr_struct.cpp +++ b/src/util/simplify_expr_struct.cpp @@ -8,15 +8,12 @@ Author: Daniel Kroening, kroening@kroening.com #include "simplify_expr_class.h" -#include - +#include "arith_tools.h" +#include "base_type.h" #include "byte_operators.h" -#include "expr.h" #include "namespace.h" -#include "std_expr.h" #include "pointer_offset_size.h" -#include "arith_tools.h" -#include "base_type.h" +#include "std_expr.h" bool simplify_exprt::simplify_member(exprt &expr) { diff --git a/src/util/ssa_expr.h b/src/util/ssa_expr.h index 63e6dfaf7d7..3a0e3b151d6 100644 --- a/src/util/ssa_expr.h +++ b/src/util/ssa_expr.h @@ -10,7 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_SSA_EXPR_H #define CPROVER_UTIL_SSA_EXPR_H -#include +#include "std_expr.h" /*! \brief Expression providing an SSA-renamed symbol of expressions */ diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp index 445c31c3c27..431ca387530 100644 --- a/src/util/std_expr.cpp +++ b/src/util/std_expr.cpp @@ -13,9 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "arith_tools.h" #include "byte_operators.h" #include "c_types.h" -#include "namespace.h" #include "pointer_offset_size.h" -#include "std_types.h" bool constant_exprt::value_is_zero_string() const { diff --git a/src/util/string_expr.h b/src/util/string_expr.h index c9d54470d3b..dd44684140f 100644 --- a/src/util/string_expr.h +++ b/src/util/string_expr.h @@ -12,9 +12,9 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #ifndef CPROVER_UTIL_STRING_EXPR_H #define CPROVER_UTIL_STRING_EXPR_H -#include -#include -#include +#include "arith_tools.h" +#include "refined_string_type.h" +#include "std_expr.h" // Given an representation of strings as exprt that implements `length` and // `content` this provides additional useful methods. diff --git a/src/util/symbol_table_base.h b/src/util/symbol_table_base.h index 62db57c024c..6a51a34a863 100644 --- a/src/util/symbol_table_base.h +++ b/src/util/symbol_table_base.h @@ -6,13 +6,9 @@ #ifndef CPROVER_UTIL_SYMBOL_TABLE_BASE_H #define CPROVER_UTIL_SYMBOL_TABLE_BASE_H -#include -#include #include #include -#include - #include "symbol.h" typedef std::multimap symbol_base_mapt; diff --git a/src/util/union_find_replace.h b/src/util/union_find_replace.h index 37f86604f1b..b7630db11ed 100644 --- a/src/util/union_find_replace.h +++ b/src/util/union_find_replace.h @@ -9,7 +9,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #ifndef CPROVER_UTIL_UNION_FIND_REPLACE_H #define CPROVER_UTIL_UNION_FIND_REPLACE_H -#include +#include "replace_expr.h" /// Similar interface to union-find for expressions, with a function for /// replacing sub-expressions by their result for find.