Move asserts to invariants (and provide suitable includes)

Author: tautschnig

src/cpp/cpp_exception_id.cpp

@@ -11,6 +11,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #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_name.h

@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #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, kroening@cs.cmu.edu
 #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);
 }
 

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 <util/invariant.h>
 #include <util/type.h>
 #include <util/expr.h>
 
@@ -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<template_typet &>(type);
 }
 
 inline const template_typet &to_template_type(const typet &type)
 {
-  assert(type.id()==ID_template);
+  PRECONDITION(type.id() == ID_template);
   return static_cast<const template_typet &>(type);
 }
 

src/cpp/cpp_token_buffer.h

@@ -16,6 +16,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 
 #include <list>
 
+#include <util/invariant.h>
+
 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 &current_token()
   {
-    assert(!tokens.empty());
+    PRECONDITION(!tokens.empty());
     return tokens.back();
   }
 

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);
   }
 }

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);