Fix linter errors, ignoring big-int and miniz

reuk · reuk · commit 52e57653e181 · 2017-07-20T13:53:53.000+01:00
diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp
@@ -463,7 +463,8 @@ void rw_range_sett::add(
 {
   objectst::iterator entry=(mode==get_modet::LHS_W ? w_range_set : r_range_set).
     insert(
-      std::pair<const irep_idt&, range_domain_baset*>(identifier, nullptr)).first;
+      std::pair<const irep_idt&, range_domain_baset*>(
+        identifier, nullptr)).first;
 
   if(entry->second==nullptr)
     entry->second=new range_domaint();
@@ -663,7 +664,8 @@ void rw_guarded_range_set_value_sett::add(
 {
   objectst::iterator entry=(mode==get_modet::LHS_W ? w_range_set : r_range_set).
     insert(
-      std::pair<const irep_idt&, range_domain_baset*>(identifier, nullptr)).first;
+      std::pair<const irep_idt&, range_domain_baset*>(
+        identifier, nullptr)).first;
 
   if(entry->second==nullptr)
     entry->second=new guarded_range_domaint();
diff --git a/src/analyses/goto_rw.h b/src/analyses/goto_rw.h
@@ -108,7 +108,7 @@ class rw_range_sett
 
   const range_domaint &get_ranges(objectst::const_iterator it) const
   {
-    assert(dynamic_cast<range_domaint*>(it->second)!=nullptr);
+    PRECONDITION(dynamic_cast<range_domaint*>(it->second)!=nullptr);
     return *static_cast<range_domaint*>(it->second);
   }
 
@@ -277,7 +277,7 @@ class rw_guarded_range_set_value_sett:public rw_range_set_value_sett
 
   const guarded_range_domaint &get_ranges(objectst::const_iterator it) const
   {
-    assert(dynamic_cast<guarded_range_domaint*>(it->second)!=nullptr);
+    PRECONDITION(dynamic_cast<guarded_range_domaint*>(it->second)!=nullptr);
     return *static_cast<guarded_range_domaint*>(it->second);
   }
 
diff --git a/src/analyses/invariant_set.cpp b/src/analyses/invariant_set.cpp
@@ -144,7 +144,7 @@ bool invariant_sett::get_object(
   const exprt &expr,
   unsigned &n) const
 {
-  assert(object_store!=nullptr);
+  PRECONDITION(object_store!=nullptr);
   return object_store->get(expr, n);
 }
 
@@ -315,7 +315,8 @@ void invariant_sett::output(
     return;
   }
 
-  assert(object_store!=nullptr);
+  INVARIANT(
+    object_store!=nullptr, nullptr_exceptiont("Object store is null"));
 
   for(unsigned i=0; i<eq_set.size(); i++)
     if(eq_set.is_root(i) &&
@@ -899,7 +900,7 @@ std::string invariant_sett::to_string(
   unsigned a,
   const irep_idt &identifier) const
 {
-  assert(object_store!=nullptr);
+  PRECONDITION(object_store!=nullptr);
   return object_store->to_string(a, identifier);
 }
 
diff --git a/src/analyses/invariant_set.h b/src/analyses/invariant_set.h
@@ -22,6 +22,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "interval_template.h"
 
+#define nullptr_exceptiont(str) str
+
 class inv_object_storet
 {
 public:
diff --git a/src/analyses/local_may_alias.h b/src/analyses/local_may_alias.h
@@ -109,7 +109,7 @@ class local_may_alias_factoryt
 
   local_may_aliast &operator()(const irep_idt &fkt)
   {
-    assert(goto_functions!=nullptr);
+    PRECONDITION(goto_functions!=nullptr);
     fkt_mapt::iterator f_it=fkt_map.find(fkt);
     if(f_it!=fkt_map.end())
       return *f_it->second;
diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp
@@ -51,7 +51,9 @@ void rd_range_domaint::transform(
 {
   reaching_definitions_analysist *rd=
     dynamic_cast<reaching_definitions_analysist*>(&ai);
-  assert(rd!=nullptr);
+  INVARIANT(
+    rd!=nullptr,
+    bad_cast_exceptiont("ai has type reaching_definitions_analysist"));
 
   assert(bv_container);
 
@@ -298,7 +300,9 @@ void rd_range_domaint::transform_assign(
     const symbolt *symbol_ptr;
     if(ns.lookup(identifier, symbol_ptr))
       continue;
-    assert(symbol_ptr!=nullptr);
+    INVARIANT(
+      symbol_ptr!=nullptr,
+      nullptr_exceptiont("Symbol is in symbol table"));
 
     const range_domaint &ranges=rw_set.get_ranges(it);
 
diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h
@@ -26,6 +26,9 @@ class is_threadedt;
 class dirtyt;
 class reaching_definitions_analysist;
 
+#define bad_cast_exceptiont(str) str
+#define nullptr_exceptiont(str) str
+
 // requirement: V has a member "identifier" of type irep_idt
 template<typename V>
 class sparse_bitvector_analysist
@@ -259,7 +262,9 @@ class reaching_definitions_analysist:
     statet &s=concurrency_aware_ait<rd_range_domaint>::get_state(l);
 
     rd_range_domaint *rd_state=dynamic_cast<rd_range_domaint*>(&s);
-    assert(rd_state!=nullptr);
+    INVARIANT(
+      rd_state!=nullptr,
+      bad_cast_exceptiont("rd_state has type rd_range_domaint"));
 
     rd_state->set_bitvector_container(*this);
 
diff --git a/src/cpp/cpp_id.h b/src/cpp/cpp_id.h
@@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <iosfwd>
 
 #include <util/expr.h>
+#include <util/invariant.h>
 #include <util/std_types.h>
 
 class cpp_scopet;
@@ -81,7 +82,7 @@ class cpp_idt
 
   cpp_idt &get_parent() const
   {
-    assert(parent!=nullptr);
+    PRECONDITION(parent!=nullptr);
     return *parent;
   }
 
diff --git a/src/cpp/cpp_instantiate_template.cpp b/src/cpp/cpp_instantiate_template.cpp
@@ -130,7 +130,8 @@ const symbolt &cpp_typecheckt::class_template_symbol(
   cpp_scopet *template_scope=
     static_cast<cpp_scopet *>(cpp_scopes.id_map[template_symbol.name]);
 
-  assert(template_scope!=nullptr);
+  INVARIANT(
+    template_scope!=nullptr, nullptr_exceptiont("template_scope is null"));
 
   irep_idt identifier=
     id2string(template_scope->prefix)+
@@ -284,7 +285,8 @@ const symbolt &cpp_typecheckt::instantiate_template(
     throw 0;
   }
 
-  assert(template_scope!=nullptr);
+  INVARIANT(
+    template_scope!=nullptr, nullptr_exceptiont("template_scope is null"));
 
   // produce new declaration
   cpp_declarationt new_decl=to_cpp_declaration(template_symbol.type);
diff --git a/src/cpp/cpp_typecheck.h b/src/cpp/cpp_typecheck.h
@@ -30,6 +30,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include "cpp_template_type.h"
 #include "cpp_util.h"
 
+#define nullptr_exceptiont(str) str
+
 bool cpp_typecheck(
   cpp_parse_treet &cpp_parse_tree,
   symbol_tablet &symbol_table,
diff --git a/src/cpp/cpp_typecheck_template.cpp b/src/cpp/cpp_typecheck_template.cpp
@@ -910,7 +910,8 @@ cpp_template_args_tct cpp_typecheckt::typecheck_template_args(
       // these need to be typechecked in the scope of the template,
       // not in the current scope!
       cpp_idt *template_scope=cpp_scopes.id_map[template_symbol.name];
-      assert(template_scope!=nullptr);
+      INVARIANT(
+        template_scope!=nullptr, nullptr_exceptiont("template_scope is null"));
       cpp_scopes.go_to(*template_scope);
     }
 
@@ -960,7 +961,9 @@ cpp_template_args_tct cpp_typecheckt::typecheck_template_args(
       {
         cpp_save_scopet cpp_saved_scope(cpp_scopes);
         cpp_idt *template_scope=cpp_scopes.id_map[template_symbol.name];
-        assert(template_scope!=nullptr);
+        INVARIANT(
+          template_scope!=nullptr,
+          nullptr_exceptiont("template_scope is null"));
         cpp_scopes.go_to(*template_scope);
         typecheck_type(type);
       }
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
@@ -541,7 +541,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
     return false;
 
   // is it a shared object?
-  assert(dirty!=nullptr);
+  INVARIANT(dirty!=nullptr, nullptr_exceptiont("dirty is null"));
   const irep_idt &obj_identifier=expr.get_object_name();
   if(obj_identifier=="goto_symex::\\guard" ||
      (!ns.lookup(obj_identifier).is_shared() &&
@@ -666,7 +666,7 @@ bool goto_symex_statet::l2_thread_read_encoding(
   expr=ssa_l1;
 
   // and record that
-  assert(symex_target!=nullptr);
+  INVARIANT(symex_target!=nullptr, nullptr_exceptiont("symex_target is null"));
   symex_target->shared_read(
     guard.as_expr(),
     expr,
@@ -685,7 +685,7 @@ bool goto_symex_statet::l2_thread_write_encoding(
     return false;
 
   // is it a shared object?
-  assert(dirty!=nullptr);
+  INVARIANT(dirty!=nullptr, nullptr_exceptiont("dirty is null"));
   const irep_idt &obj_identifier=expr.get_object_name();
   if(obj_identifier=="goto_symex::\\guard" ||
      (!ns.lookup(obj_identifier).is_shared() &&
diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h
@@ -26,6 +26,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 class dirtyt;
 
+#define nullptr_exceptiont(str) str
+
 // central data structure: state
 class goto_symex_statet
 {
diff --git a/src/path-symex/path_symex_history.h b/src/path-symex/path_symex_history.h
@@ -21,6 +21,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 class path_symex_stept;
 
+#define nullptr_exceptiont(str) str
+
 // This is a reference to a path_symex_stept,
 // and is really cheap to copy. These references are stable,
 // even though the underlying vector is not.
@@ -46,7 +48,7 @@ class path_symex_step_reft
 
   path_symex_historyt &get_history() const
   {
-    assert(history!=nullptr);
+    INVARIANT(history!=nullptr, nullptr_exceptiont("history is null"));
     return *history;
   }
 
@@ -154,7 +156,7 @@ class path_symex_historyt
 
 inline void path_symex_step_reft::generate_successor()
 {
-  assert(history!=nullptr);
+  INVARIANT(history!=nullptr, nullptr_exceptiont("history is null"));
   path_symex_step_reft old=*this;
   index=history->step_container.size();
   history->step_container.push_back(path_symex_stept());
@@ -169,7 +171,7 @@ inline path_symex_step_reft &path_symex_step_reft::operator--()
 
 inline path_symex_stept &path_symex_step_reft::get() const
 {
-  assert(history!=nullptr);
+  INVARIANT(history!=nullptr, nullptr_exceptiont("history is null"));
   assert(!is_nil());
   return history->step_container[index];
 }
diff --git a/src/path-symex/path_symex_state.h b/src/path-symex/path_symex_state.h
@@ -16,6 +16,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "var_map.h"
 #include "path_symex_history.h"
 
+#define nullptr_exceptiont(str) str
+
 struct path_symex_statet
 {
 public:
diff --git a/src/path-symex/path_symex_state_read.cpp b/src/path-symex/path_symex_state_read.cpp
@@ -465,7 +465,7 @@ bool path_symex_statet::is_symbol_member_index(const exprt &src) const
       return false;
 
     // next round
-    assert(next!=nullptr);
+    INVARIANT(next!=nullptr, nullptr_exceptiont("next is null"));
     current=next;
   }
 }

Original file line number	Diff line number	Diff line change
`@@ -108,7 +108,7 @@ class rw_range_sett`
`108`	`108`
`109`	`109`	`const range_domaint &get_ranges(objectst::const_iterator it) const`
`110`	`110`	`{`
`111`		`- assert(dynamic_cast<range_domaint*>(it->second)!=nullptr);`
	`111`	`+ PRECONDITION(dynamic_cast<range_domaint*>(it->second)!=nullptr);`
`112`	`112`	`return static_cast<range_domaint>(it->second);`
`113`	`113`	`}`
`114`	`114`
`@@ -277,7 +277,7 @@ class rw_guarded_range_set_value_sett:public rw_range_set_value_sett`
`277`	`277`
`278`	`278`	`const guarded_range_domaint &get_ranges(objectst::const_iterator it) const`
`279`	`279`	`{`
`280`		`- assert(dynamic_cast<guarded_range_domaint*>(it->second)!=nullptr);`
	`280`	`+ PRECONDITION(dynamic_cast<guarded_range_domaint*>(it->second)!=nullptr);`
`281`	`281`	`return static_cast<guarded_range_domaint>(it->second);`
`282`	`282`	`}`
`283`	`283`
Original file line number	Diff line number	Diff line change
`@@ -144,7 +144,7 @@ bool invariant_sett::get_object(`
`144`	`144`	`const exprt &expr,`
`145`	`145`	`unsigned &n) const`
`146`	`146`	`{`
`147`		`- assert(object_store!=nullptr);`
	`147`	`+ PRECONDITION(object_store!=nullptr);`
`148`	`148`	`return object_store->get(expr, n);`
`149`	`149`	`}`
`150`	`150`
`@@ -315,7 +315,8 @@ void invariant_sett::output(`
`315`	`315`	`return;`
`316`	`316`	`}`
`317`	`317`
`318`		`- assert(object_store!=nullptr);`
	`318`	`+ INVARIANT(`
	`319`	`+ object_store!=nullptr, nullptr_exceptiont("Object store is null"));`
`319`	`320`
`320`	`321`	`for(unsigned i=0; i<eq_set.size(); i++)`
`321`	`322`	`if(eq_set.is_root(i) &&`
`@@ -899,7 +900,7 @@ std::string invariant_sett::to_string(`
`899`	`900`	`unsigned a,`
`900`	`901`	`const irep_idt &identifier) const`
`901`	`902`	`{`
`902`		`- assert(object_store!=nullptr);`
	`903`	`+ PRECONDITION(object_store!=nullptr);`
`903`	`904`	`return object_store->to_string(a, identifier);`
`904`	`905`	`}`
`905`	`906`
Original file line number	Diff line number	Diff line change
`@@ -22,6 +22,8 @@ Author: Daniel Kroening, kroening@kroening.com`
`22`	`22`
`23`	`23`	`#include "interval_template.h"`
`24`	`24`
	`25`	`+#define nullptr_exceptiont(str) str`
	`26`	`+`
`25`	`27`	`class inv_object_storet`
`26`	`28`	`{`
`27`	`29`	`public:`
Original file line number	Diff line number	Diff line change
`@@ -109,7 +109,7 @@ class local_may_alias_factoryt`
`109`	`109`
`110`	`110`	`local_may_aliast &operator()(const irep_idt &fkt)`
`111`	`111`	`{`
`112`		`- assert(goto_functions!=nullptr);`
	`112`	`+ PRECONDITION(goto_functions!=nullptr);`
`113`	`113`	`fkt_mapt::iterator f_it=fkt_map.find(fkt);`
`114`	`114`	`if(f_it!=fkt_map.end())`
`115`	`115`	`return *f_it->second;`
Original file line number	Diff line number	Diff line change
`@@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu`
`20`	`20`	`#include <iosfwd>`
`21`	`21`
`22`	`22`	`#include <util/expr.h>`
	`23`	`+#include <util/invariant.h>`
`23`	`24`	`#include <util/std_types.h>`
`24`	`25`
`25`	`26`	`class cpp_scopet;`
`@@ -81,7 +82,7 @@ class cpp_idt`
`81`	`82`
`82`	`83`	`cpp_idt &get_parent() const`
`83`	`84`	`{`
`84`		`- assert(parent!=nullptr);`
	`85`	`+ PRECONDITION(parent!=nullptr);`
`85`	`86`	`return *parent;`
`86`	`87`	`}`
`87`	`88`