Enable compilation with NDEBUG defined

Compilation used to fail since NDEBUG removes assertions, leading to
unused variables. The commit replaces these assertions with INVARIANT or
a derivative.

Author: andreast271

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -236,7 +236,7 @@ exprt c_nondet_symbol_factory(
 
   symbolt *main_symbol_ptr;
   bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr);
-  assert(!moving_symbol_failed);
+  CHECK_RETURN(!moving_symbol_failed);
 
   std::vector<symbolt const *> symbols_created;
   symbol_exprt main_symbol_expr=(*main_symbol_ptr).symbol_expr();

src/ansi-c/c_typecheck_initializer.cpp

@@ -33,10 +33,10 @@ void c_typecheck_baset::do_initializer(
 
   if(type.id()==ID_array)
   {
-    // any arrays must have a size
     const typet &result_type=follow(result.type());
-    assert(result_type.id()==ID_array &&
-           to_array_type(result_type).size().is_not_nil());
+    DATA_INVARIANT(result_type.id()==ID_array &&
+                   to_array_type(result_type).size().is_not_nil(),
+                   "any array must have a size");
 
     // we don't allow initialisation with symbols of array type
     if(result.id()!=ID_array)
@@ -436,9 +436,11 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
         throw 0;
       }
 
-      assert(index<components.size());
-      assert(components[index].type().id()!=ID_code &&
-             !components[index].get_is_padding());
+      DATA_INVARIANT(index<components.size(),
+                     "member designator is bounded by components size");
+      DATA_INVARIANT(components[index].type().id()!=ID_code &&
+                     !components[index].get_is_padding(),
+                     "member designator points at data member");
 
       dest=&(dest->operands()[index]);
     }
@@ -449,7 +451,8 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
       const union_typet::componentst &components=
         union_type.components();
 
-      assert(index<components.size());
+      DATA_INVARIANT(index<components.size(),
+                     "member designator is bounded by components size");
 
       const union_typet::componentt &component=union_type.components()[index];
 

src/cpp/cpp_typecheck_compound_type.cpp

@@ -537,7 +537,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
         vt_symb_type.is_type=true;
 
         const bool failed=!symbol_table.insert(std::move(vt_symb_type)).second;
-        assert(!failed);
+        CHECK_RETURN(!failed);
 
         // add a virtual-table pointer
         struct_typet::componentt compo;
@@ -613,7 +613,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
 
           // add the parameter to the symbol table
           const bool failed=!symbol_table.insert(std::move(arg_symb)).second;
-          assert(!failed);
+          CHECK_RETURN(!failed);
         }
 
         // do the body of the function
@@ -671,7 +671,7 @@ void cpp_typecheckt::typecheck_compound_declarator(
         // add the function to the symbol table
         {
           const bool failed=!symbol_table.insert(std::move(func_symb)).second;
-          assert(!failed);
+          CHECK_RETURN(!failed);
         }
 
         // next base

src/cpp/cpp_typecheck_constructor.cpp

@@ -486,8 +486,8 @@ void cpp_typecheckt::default_assignop_value(
 
       mp_integer size;
       bool to_int=to_integer(size_expr, size);
-      assert(!to_int);
-      assert(size>=0);
+      CHECK_RETURN(!to_int);
+      CHECK_RETURN(size>=0);
 
       exprt::operandst empty_operands;
       for(mp_integer i=0; i < size; ++i)

src/cpp/cpp_typecheck_initializer.cpp

@@ -215,8 +215,8 @@ void cpp_typecheckt::zero_initializer(
     mp_integer size;
 
     bool to_int=to_integer(size_expr, size);
-    assert(!to_int);
-    assert(size>=0);
+    CHECK_RETURN(!to_int);
+    CHECK_RETURN(size>=0);
 
     exprt::operandst empty_operands;
     for(mp_integer i=0; i<size; ++i)

src/cpp/cpp_typecheck_resolve.cpp

@@ -2125,7 +2125,8 @@ void cpp_typecheck_resolvet::apply_template_args(
         const struct_typet &struct_type=
           to_struct_type(type_symb.type);
 
-        assert(struct_type.has_component(new_symbol.name));
+        DATA_INVARIANT(struct_type.has_component(new_symbol.name),
+                       "method should exist in struct");
         member_exprt member(code_type);
         member.set_component_name(new_symbol.name);
         member.struct_op()=*fargs.operands.begin();

src/cpp/cpp_typecheck_virtual_table.cpp

@@ -96,6 +96,6 @@ void cpp_typecheckt::do_virtual_table(const symbolt &symbol)
     vt_symb_var.value=values;
 
     bool failed=!symbol_table.insert(std::move(vt_symb_var)).second;
-    assert(!failed);
+    CHECK_RETURN(!failed);
   }
 }

src/goto-instrument/accelerate/polynomial.cpp

@@ -409,7 +409,7 @@ int monomialt::compare(monomialt &other)
     return -1;
   }
 
-  assert(!"NOTREACHEDBITCHES");
+  UNREACHABLE;
 }
 
 int polynomialt::max_degree(const exprt &var)

src/goto-instrument/accelerate/util.cpp

@@ -117,5 +117,6 @@ typet join_types(const typet &t1, const typet &t2)
   std::cerr << "Tried to join types: "
             << t1.pretty() << " and " << t2.pretty()
             << '\n';
-  assert(!"Couldn't join types");
+
+  INVARIANT(false, "failed to join types");
 }

src/goto-instrument/full_slicer.cpp

@@ -185,7 +185,8 @@ void full_slicert::add_jumps(
         if(cfg[entry->second].node_required)
         {
           const irep_idt id2=goto_programt::get_function_id(*d_it);
-          assert(id==id2);
+          INVARIANT(id==id2,
+                    "goto/jump expected to be within a single function");
 
           cfg_post_dominatorst::cfgt::entry_mapt::const_iterator e2=
             pd.cfg.entry_map.find(*d_it);