Merge pull request #5602 from tautschnig/cleanup-cassert

tautschnig · web-flow · commit f0a22a78df34 · 2020-11-18T22:45:26.000+01:00
Remove unnecessary cassert include
diff --git a/jbmc/src/java_bytecode/expr2java.cpp b/jbmc/src/java_bytecode/expr2java.cpp
@@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include "expr2java.h"
 
-#include <cassert>
 #include <sstream>
 
 #include <util/namespace.h>
diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp
@@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "ai.h"
 
-#include <cassert>
 #include <memory>
 #include <sstream>
 #include <type_traits>
diff --git a/src/analyses/cfg_dominators.h b/src/analyses/cfg_dominators.h
@@ -16,7 +16,6 @@ Author: Georg Weissenbacher, georg@weissenbacher.name
 #include <list>
 #include <map>
 #include <iosfwd>
-#include <cassert>
 
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/goto_program.h>
diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp
@@ -14,8 +14,6 @@ Date: August 2013
 
 #include "dependence_graph.h"
 
-#include <cassert>
-
 #include <util/container_utils.h>
 #include <util/json_irep.h>
 
diff --git a/src/analyses/flow_insensitive_analysis.cpp b/src/analyses/flow_insensitive_analysis.cpp
@@ -12,8 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "flow_insensitive_analysis.h"
 
-#include <cassert>
-
 #include <util/expr_util.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
diff --git a/src/analyses/static_analysis.cpp b/src/analyses/static_analysis.cpp
@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #define USE_DEPRECATED_STATIC_ANALYSIS_H
 #include "static_analysis.h"
 
-#include <cassert>
 #include <memory>
 
 #include <util/expr_util.h>
diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp
@@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "ansi_c_convert_type.h"
 
-#include <cassert>
-
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
diff --git a/src/ansi-c/ansi_c_declaration.cpp b/src/ansi-c/ansi_c_declaration.cpp
@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "ansi_c_declaration.h"
 
 #include <ostream>
-#include <cassert>
 
 #include <util/config.h>
 #include <util/std_types.h>
diff --git a/src/ansi-c/ansi_c_declaration.h b/src/ansi-c/ansi_c_declaration.h
@@ -12,8 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_ANSI_C_ANSI_C_DECLARATION_H
 #define CPROVER_ANSI_C_ANSI_C_DECLARATION_H
 
-#include <cassert>
-
 #include <util/std_expr.h>
 #include <util/symbol.h>
 
diff --git a/src/ansi-c/ansi_c_parser.h b/src/ansi-c/ansi_c_parser.h
@@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_ANSI_C_ANSI_C_PARSER_H
 #define CPROVER_ANSI_C_ANSI_C_PARSER_H
 
-#include <cassert>
 #include <set>
 
 #include <util/parser.h>
diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp
@@ -10,8 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <algorithm>
 
-#include <cassert>
-
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
@@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "c_typecheck_base.h"
 
-#include <cassert>
 #include <sstream>
 
 #include <util/arith_tools.h>
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
@@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "expr2c.h"
 
 #include <algorithm>
-#include <cassert>
 #include <sstream>
 
 #include <map>
diff --git a/src/ansi-c/literals/convert_character_literal.cpp b/src/ansi-c/literals/convert_character_literal.cpp
@@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "convert_character_literal.h"
 
-#include <cassert>
-
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/std_expr.h>
diff --git a/src/ansi-c/literals/convert_float_literal.cpp b/src/ansi-c/literals/convert_float_literal.cpp
@@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "convert_float_literal.h"
 
-#include <cassert>
-
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/ieee_float.h>
diff --git a/src/ansi-c/literals/convert_integer_literal.cpp b/src/ansi-c/literals/convert_integer_literal.cpp
@@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "convert_integer_literal.h"
 
-#include <cassert>
 #include <cctype>
 
 #include <util/arith_tools.h>
diff --git a/src/ansi-c/literals/convert_string_literal.cpp b/src/ansi-c/literals/convert_string_literal.cpp
@@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "convert_string_literal.h"
 
-#include <cassert>
-
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/unicode.h>
diff --git a/src/ansi-c/literals/unescape_string.cpp b/src/ansi-c/literals/unescape_string.cpp
@@ -11,9 +11,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "unescape_string.h"
 
-#include <cassert>
 #include <cctype>
 
+#include <util/invariant.h>
 #include <util/unicode.h>
 
 static void append_universal_char(
@@ -50,7 +50,7 @@ std::basic_string<T> unescape_string_templ(const std::string &src)
     {
       // go to next character
       i++;
-      assert(i<src.size()); // backslash can't be last character
+      INVARIANT(i < src.size(), "backslash can't be last character");
 
       ch=(unsigned char)src[i];
       switch(ch)
diff --git a/src/cpp/cpp_convert_type.cpp b/src/cpp/cpp_convert_type.cpp
@@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include "cpp_convert_type.h"
 
-#include <cassert>
-
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
diff --git a/src/cpp/cpp_declaration.h b/src/cpp/cpp_declaration.h
@@ -12,8 +12,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #ifndef CPROVER_CPP_CPP_DECLARATION_H
 #define CPROVER_CPP_CPP_DECLARATION_H
 
-#include <cassert>
-
 #include "cpp_declarator.h"
 #include "cpp_storage_spec.h"
 #include "cpp_member_spec.h"
diff --git a/src/cpp/cpp_declarator.cpp b/src/cpp/cpp_declarator.cpp
@@ -14,7 +14,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <ansi-c/merged_type.h>
 
 #include <ostream>
-#include <cassert>
 
 void cpp_declaratort::output(std::ostream &out) const
 {
diff --git a/src/cpp/cpp_enum_type.h b/src/cpp/cpp_enum_type.h
@@ -12,8 +12,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #ifndef CPROVER_CPP_CPP_ENUM_TYPE_H
 #define CPROVER_CPP_CPP_ENUM_TYPE_H
 
-#include <cassert>
-
 #include <util/type.h>
 
 #include "cpp_name.h"
diff --git a/src/cpp/cpp_id.h b/src/cpp/cpp_id.h
@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #ifndef CPROVER_CPP_CPP_ID_H
 #define CPROVER_CPP_CPP_ID_H
 
-#include <cassert>
 #include <list>
 #include <map>
 #include <string>
diff --git a/src/cpp/cpp_item.h b/src/cpp/cpp_item.h
@@ -12,8 +12,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #ifndef CPROVER_CPP_CPP_ITEM_H
 #define CPROVER_CPP_CPP_ITEM_H
 
-#include <cassert>
-
 #include "cpp_declaration.h"
 #include "cpp_linkage_spec.h"
 #include "cpp_namespace_spec.h"
diff --git a/src/cpp/cpp_name.cpp b/src/cpp/cpp_name.cpp
@@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include "cpp_name.h"
 
-#include <cassert>
 #include <sstream>
 
 irep_idt cpp_namet::get_base_name() const
diff --git a/src/cpp/cpp_parser.h b/src/cpp/cpp_parser.h
@@ -12,8 +12,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #ifndef CPROVER_CPP_CPP_PARSER_H
 #define CPROVER_CPP_CPP_PARSER_H
 
-#include <cassert>
-
 #include <util/string_hash.h>
 #include <util/parser.h>
 #include <util/expr.h>
diff --git a/src/cpp/cpp_token_buffer.cpp b/src/cpp/cpp_token_buffer.cpp
@@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include "cpp_token_buffer.h"
 
-#include <cassert>
-
 #include <ansi-c/ansi_c_y.tab.h>
 #include <ansi-c/ansi_c_parser.h>
 
diff --git a/src/cpp/cpp_typecheck_fargs.cpp b/src/cpp/cpp_typecheck_fargs.cpp
@@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include "cpp_typecheck_fargs.h"
 
-#include <cassert>
-
 #include <util/std_types.h>
 
 #include <ansi-c/c_qualifiers.h>
diff --git a/src/cpp/cpp_typecheck_fargs.h b/src/cpp/cpp_typecheck_fargs.h
@@ -12,8 +12,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #ifndef CPROVER_CPP_CPP_TYPECHECK_FARGS_H
 #define CPROVER_CPP_CPP_TYPECHECK_FARGS_H
 
-#include <cassert>
-
 #include <util/std_code.h>
 
 class cpp_typecheckt;
diff --git a/src/cpp/expr2cpp.cpp b/src/cpp/expr2cpp.cpp
@@ -8,8 +8,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include "expr2cpp.h"
 
-#include <cassert>
-
 #include <util/std_types.h>
 #include <util/std_expr.h>
 #include <util/symbol.h>
diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp
@@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include "cpp_parser.h"
 
-#include <cassert>
 #include <map>
 
 #include <util/c_types.h>
diff --git a/src/goto-cc/as86_cmdline.cpp b/src/goto-cc/as86_cmdline.cpp
@@ -11,7 +11,6 @@ Author: Michael Tautschnig
 
 #include "as86_cmdline.h"
 
-#include <cassert>
 #include <iostream>
 
 #include <util/prefix.h>
diff --git a/src/goto-cc/as_cmdline.cpp b/src/goto-cc/as_cmdline.cpp
@@ -11,7 +11,6 @@ Author: Michael Tautschnig
 
 #include "as_cmdline.h"
 
-#include <cassert>
 #include <iostream>
 
 #include <util/prefix.h>
diff --git a/src/goto-cc/bcc_cmdline.cpp b/src/goto-cc/bcc_cmdline.cpp
@@ -11,7 +11,6 @@ Author: Michael Tautschnig
 
 #include "bcc_cmdline.h"
 
-#include <cassert>
 #include <iostream>
 
 #include <util/prefix.h>
diff --git a/src/goto-cc/gcc_cmdline.cpp b/src/goto-cc/gcc_cmdline.cpp
@@ -11,7 +11,6 @@ Author: CM Wintersteiger, 2006
 
 #include "gcc_cmdline.h"
 
-#include <cassert>
 #include <cstring>
 #include <iostream>
 #include <fstream>
diff --git a/src/goto-cc/goto_cc_cmdline.cpp b/src/goto-cc/goto_cc_cmdline.cpp
@@ -14,7 +14,6 @@ Date:   April 2010
 #include "goto_cc_cmdline.h"
 
 #include <algorithm>
-#include <cassert>
 #include <cstdio>
 #include <cstring>
 #include <iostream>
diff --git a/src/goto-cc/ld_cmdline.cpp b/src/goto-cc/ld_cmdline.cpp
@@ -11,7 +11,6 @@ Author: Daniel Kroening, 2013
 
 #include "ld_cmdline.h"
 
-#include <cassert>
 #include <iostream>
 
 #include <util/prefix.h>
diff --git a/src/goto-cc/ms_cl_cmdline.cpp b/src/goto-cc/ms_cl_cmdline.cpp
@@ -11,7 +11,6 @@ Author: Daniel Kroening
 
 #include "ms_cl_cmdline.h"
 
-#include <cassert>
 #include <cstring>
 #include <cstdlib>
 #include <iostream>
diff --git a/src/goto-cc/ms_link_cmdline.cpp b/src/goto-cc/ms_link_cmdline.cpp
@@ -11,7 +11,6 @@ Author: Daniel Kroening
 
 #include "ms_link_cmdline.h"
 
-#include <cassert>
 #include <cstdlib>
 #include <cstring>
 #include <fstream>
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
@@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_convert_class.h"
 
-#include <cassert>
-
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/cprover_prefix.h>
diff --git a/src/goto-programs/goto_inline.cpp b/src/goto-programs/goto_inline.cpp
@@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_inline.h"
 
-#include <cassert>
-
 #include <util/prefix.h>
 #include <util/cprover_prefix.h>
 #include <util/std_code.h>
diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
@@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "remove_function_pointers.h"
 
-#include <cassert>
-
 #include <util/c_types.h>
 #include <util/fresh_symbol.h>
 #include <util/invariant.h>
diff --git a/src/goto-programs/xml_goto_trace.cpp b/src/goto-programs/xml_goto_trace.cpp
@@ -13,8 +13,6 @@ Author: Daniel Kroening
 
 #include "xml_goto_trace.h"
 
-#include <cassert>
-
 #include <util/symbol.h>
 #include <util/xml_irep.h>
 
diff --git a/src/goto-symex/symex_decl.cpp b/src/goto-symex/symex_decl.cpp
@@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_symex.h"
 
-#include <cassert>
-
 #include <util/std_expr.h>
 
 void goto_symext::symex_decl(statet &state)
diff --git a/src/json/json_parser.h b/src/json/json_parser.h
@@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_JSON_JSON_PARSER_H
 #define CPROVER_JSON_JSON_PARSER_H
 
-#include <cassert>
 #include <stack>
 
 #include <util/parser.h>
diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp
diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
diff --git a/src/solvers/bdd/miniBDD/miniBDD.h b/src/solvers/bdd/miniBDD/miniBDD.h
diff --git a/src/solvers/flattening/boolbv_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp
diff --git a/src/solvers/flattening/boolbv_extractbit.cpp b/src/solvers/flattening/boolbv_extractbit.cpp
diff --git a/src/solvers/flattening/boolbv_get.cpp b/src/solvers/flattening/boolbv_get.cpp
diff --git a/src/solvers/flattening/boolbv_typecast.cpp b/src/solvers/flattening/boolbv_typecast.cpp
diff --git a/src/solvers/flattening/bv_utils.cpp b/src/solvers/flattening/bv_utils.cpp
diff --git a/src/util/endianness_map.h b/src/util/endianness_map.h
diff --git a/src/util/graph.h b/src/util/graph.h
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp
diff --git a/src/util/ssa_expr.cpp b/src/util/ssa_expr.cpp
diff --git a/src/util/string_utils.cpp b/src/util/string_utils.cpp
diff --git a/src/util/union_find.h b/src/util/union_find.h
diff --git a/src/xmllang/graphml.cpp b/src/xmllang/graphml.cpp
