Cleanup of unnecessary includes, plus other cleanups

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 <map>
-#include <ostream>
+#include <iosfwd>
 #include <limits>
+#include <map>
 #include <memory> // unique_ptr
 
 #include <util/guard.h>

src/ansi-c/ansi_c_entry_point.cpp

@@ -8,21 +8,13 @@ Author: Daniel Kroening, [email protected]
 
 #include "ansi_c_entry_point.h"
 
-#include <cassert>
-#include <cstdlib>
-
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
-#include <util/cprover_prefix.h>
-#include <util/namespace.h>
-#include <util/prefix.h>
-#include <util/std_code.h>
-#include <util/std_expr.h>
 #include <util/string_constant.h>
-#include <util/symbol.h>
 
 #include <goto-programs/goto_functions.h>
+
 #include <linking/static_lifetime_init.h>
 
 #include "c_nondet_symbol_factory.h"
@@ -217,7 +209,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;
     }

src/ansi-c/ansi_c_internal_additions.cpp

@@ -10,6 +10,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/config.h>
 
+#include <linking/static_lifetime_init.h>
+
 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

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -11,22 +11,14 @@ Author: Diffblue Ltd.
 
 #include "c_nondet_symbol_factory.h"
 
-#include <set>
-#include <sstream>
-
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/fresh_symbol.h>
 #include <util/namespace.h>
-#include <util/pointer_offset_size.h>
-#include <util/prefix.h>
-#include <util/std_code.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
 #include <util/string_constant.h>
 
-#include <linking/zero_initializer.h>
-
 #include <goto-programs/goto_functions.h>
 
 /// Create a new temporary static symbol

src/ansi-c/c_typecheck_expr.cpp

@@ -14,17 +14,14 @@ Author: Daniel Kroening, [email protected]
 #include <cassert>
 
 #include <util/arith_tools.h>
+#include <util/base_type.h>
 #include <util/c_types.h>
-#include <util/config.h>
-#include <util/std_types.h>
-#include <util/prefix.h>
 #include <util/cprover_prefix.h>
-#include <util/simplify_expr.h>
-#include <util/base_type.h>
-#include <util/std_expr.h>
-#include <util/string_constant.h>
+#include <util/ieee_float.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
+#include <util/simplify_expr.h>
+#include <util/string_constant.h>
 
 #include "builtin_factory.h"
 #include "c_typecast.h"

src/ansi-c/c_typecheck_type.cpp

@@ -13,19 +13,16 @@ Author: Daniel Kroening, [email protected]
 
 #include <unordered_set>
 
+#include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
-#include <util/invariant.h>
-#include <util/simplify_expr.h>
-#include <util/arith_tools.h>
-#include <util/std_types.h>
 #include <util/pointer_offset_size.h>
+#include <util/simplify_expr.h>
 
+#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)
 {

src/ansi-c/expr2c.cpp

@@ -10,33 +10,21 @@ Author: Daniel Kroening, [email protected]
 
 #include <algorithm>
 #include <cassert>
-#include <cctype>
-#include <cstdio>
-
-#ifdef _WIN32
-#ifndef __MINGW32__
-#define snprintf sprintf_s
-#endif
-#endif
+#include <sstream>
 
 #include <map>
-#include <set>
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
-#include <util/std_types.h>
-#include <util/std_code.h>
-#include <util/ieee_float.h>
+#include <util/find_symbols.h>
 #include <util/fixedbv.h>
-#include <util/prefix.h>
-#include <util/lispirep.h>
 #include <util/lispexpr.h>
+#include <util/lispirep.h>
 #include <util/namespace.h>
-#include <util/symbol.h>
-#include <util/suffix.h>
-#include <util/find_symbols.h>
 #include <util/pointer_offset_size.h>
+#include <util/suffix.h>
+#include <util/symbol.h>
 
 #include "c_misc.h"
 #include "c_qualifiers.h"
@@ -2258,9 +2246,9 @@ std::string expr2ct::convert_array(
           dest+=static_cast<char>(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;
         }
       }

src/ansi-c/type2name.cpp

@@ -11,13 +11,12 @@ Author: Daniel Kroening, [email protected]
 
 #include "type2name.h"
 
-#include <util/std_types.h>
 #include <util/arith_tools.h>
+#include <util/invariant.h>
 #include <util/namespace.h>
-#include <util/symbol.h>
-#include <util/symbol_table.h>
 #include <util/pointer_offset_size.h>
-#include <util/invariant.h>
+#include <util/std_types.h>
+#include <util/symbol_table.h>
 
 typedef std::unordered_map<irep_idt, std::pair<size_t, bool>> symbol_numbert;
 

src/cbmc/bmc.cpp

@@ -12,35 +12,24 @@ Author: Daniel Kroening, [email protected]
 #include "bmc.h"
 
 #include <chrono>
-#include <exception>
-#include <fstream>
 #include <iostream>
-#include <memory>
 
 #include <util/exit_codes.h>
 #include <util/string2int.h>
-#include <util/source_location.h>
 #include <util/string_utils.h>
-#include <util/memory_info.h>
-#include <util/message.h>
-#include <util/json.h>
-#include <util/json_stream.h>
-#include <util/cprover_prefix.h>
 
-#include <langapi/mode.h>
 #include <langapi/language_util.h>
 
-#include <goto-programs/goto_model.h>
-#include <goto-programs/xml_goto_trace.h>
-#include <goto-programs/json_goto_trace.h>
 #include <goto-programs/graphml_witness.h>
+#include <goto-programs/json_goto_trace.h>
+#include <goto-programs/xml_goto_trace.h>
 
 #include <goto-symex/build_goto_trace.h>
+#include <goto-symex/memory_model_pso.h>
 #include <goto-symex/slice.h>
 #include <goto-symex/slice_by_trace.h>
-#include <goto-symex/memory_model_sc.h>
-#include <goto-symex/memory_model_tso.h>
-#include <goto-symex/memory_model_pso.h>
+
+#include <linking/static_lifetime_init.h>
 
 #include "cbmc_solvers.h"
 #include "counterexample_beautification.h"
@@ -338,7 +327,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;
   }
 

src/cbmc/symex_coverage.cpp

@@ -13,22 +13,21 @@ Date: March 2016
 
 #include "symex_coverage.h"
 
-#include <ctime>
 #include <chrono>
-#include <iostream>
+#include <ctime>
 #include <fstream>
-#include <sstream>
+#include <iostream>
 
-#include <util/xml.h>
 #include <util/string2int.h>
-#include <util/cprover_prefix.h>
-#include <util/prefix.h>
+#include <util/xml.h>
 
 #include <langapi/language_util.h>
 
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/remove_returns.h>
 
+#include <linking/static_lifetime_init.h>
+
 class coverage_recordt
 {
 public:
@@ -313,7 +312,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);

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 <string>
-#include <ostream>
+#include <iosfwd>
 #include <map>
+#include <string>
 
 #include <goto-programs/goto_program.h>
 

src/cpp/cpp_exception_id.cpp

@@ -11,6 +11,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "cpp_exception_id.h"
 
+#include <util/invariant.h>
+
 /// 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<irep_idt> ids;
   cpp_exception_list_rec(src, ns, "", ids);
-  assert(!ids.empty());
+  CHECK_RETURN(!ids.empty());
   return ids.front();
 }

src/cpp/cpp_internal_additions.cpp

@@ -14,6 +14,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <ansi-c/ansi_c_internal_additions.h>
 
+#include <linking/static_lifetime_init.h>
+
 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';

src/cpp/cpp_name.h

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_CPP_CPP_NAME_H
 
 #include <util/expr.h>
+#include <util/invariant.h>
 
 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_namet &>(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<const cpp_namet &>(cpp_name);
 }
 

src/cpp/cpp_template_args.h

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_CPP_CPP_TEMPLATE_ARGS_H
 
 #include <util/expr.h>
+#include <util/invariant.h>
 
 // A data structures for template arguments, i.e.,
 // a sequence of types/expressions of the form <E1, T2, ...>.
@@ -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<cpp_template_args_non_tct &>(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<const cpp_template_args_non_tct &>(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<cpp_template_args_tct &>(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<const cpp_template_args_tct &>(irep);
 }