Enable compilation with NDEBUG defined

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

src/goto-instrument/unwind.h

@@ -119,7 +119,7 @@ class goto_unwindt
       const unsigned location_number)
     {
       auto r=location_map.insert(std::make_pair(target, location_number));
-      assert(r.second); // did not exist yet
+      INVARIANT(r.second, "target already exists");
     }
 
     typedef std::map<goto_programt::const_targett, unsigned> location_mapt;

src/goto-instrument/wmm/event_graph.h

@@ -406,9 +406,9 @@ class event_grapht
 
   event_idt add_node()
   {
-    const event_idt po_no = po_graph.add_node();
-    const event_idt com_no = com_graph.add_node();
-    assert(po_no == com_no);
+    const event_idt po_no=po_graph.add_node();
+    const event_idt com_no=com_graph.add_node();
+    INVARIANT(po_no==com_no, "node added with same id in both graphs");
     return po_no;
   }
 

src/goto-symex/symex_dereference.cpp

@@ -221,8 +221,9 @@ exprt goto_symext::address_arithmetic(
     throw "goto_symext::address_arithmetic does not handle "+expr.id_string();
 
   const typet &expr_type=ns.follow(expr.type());
-  assert((expr_type.id()==ID_array && !keep_array) ||
-         base_type_eq(pointer_type(expr_type), result.type(), ns));
+  INVARIANT((expr_type.id()==ID_array && !keep_array) ||
+            base_type_eq(pointer_type(expr_type), result.type(), ns),
+            "either non-persistent array or pointer to result");
 
   return result;
 }

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1320,8 +1320,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
             "java::org.cprover.CProver.assume:(Z)V")
     {
       const code_typet &code_type=to_code_type(arg0.type());
-      // sanity check: function has the right number of args
-      assert(code_type.parameters().size()==1);
+      INVARIANT(code_type.parameters().size()==1,
+                "function expected to have exactly one parameter");
 
       exprt operand = pop(1)[0];
       // we may need to adjust the type of the argument
@@ -1384,7 +1384,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
       if(use_this)
       {
         const exprt &this_arg=call.arguments().front();
-        assert(this_arg.type().id()==ID_pointer);
+        INVARIANT(this_arg.type().id()==ID_pointer,
+                  "first argument must be a pointer");
       }
 
       // do some type adjustment for the arguments,

src/java_bytecode/java_bytecode_parser.cpp

@@ -635,7 +635,7 @@ void java_bytecode_parsert::rfields(classt &parsed_class)
     size_t flags=(field.is_public?1:0)+
       (field.is_protected?1:0)+
       (field.is_private?1:0);
-    assert(flags<=1);
+    DATA_INVARIANT(flags<=1, "at most one of public, protected, private");
 
     for(std::size_t j=0; j<attributes_count; j++)
       rfield_attribute(field);
@@ -1361,7 +1361,7 @@ void java_bytecode_parsert::rmethod(classt &parsed_class)
   size_t flags=(method.is_public?1:0)+
     (method.is_protected?1:0)+
     (method.is_private?1:0);
-  assert(flags<=1);
+  DATA_INVARIANT(flags<=1, "at most one of public, protected, private");
   u2 attributes_count=read_u2();
 
   for(std::size_t j=0; j<attributes_count; j++)

src/pointer-analysis/value_set.cpp

@@ -369,8 +369,9 @@ void value_sett::get_value_set_rec(
 
     const typet &type=ns.follow(expr.op0().type());
 
-    assert(type.id()==ID_array ||
-           type.id()==ID_incomplete_array);
+    DATA_INVARIANT(type.id()==ID_array ||
+                   type.id()==ID_incomplete_array,
+                   "operand 0 of index expression must be an array");
 
     get_value_set_rec(expr.op0(), dest, "[]"+suffix, original_type, ns);
   }
@@ -380,10 +381,11 @@ void value_sett::get_value_set_rec(
 
     const typet &type=ns.follow(expr.op0().type());
 
-    assert(type.id()==ID_struct ||
-           type.id()==ID_union ||
-           type.id()==ID_incomplete_struct ||
-           type.id()==ID_incomplete_union);
+    DATA_INVARIANT(type.id()==ID_struct ||
+                   type.id()==ID_union ||
+                   type.id()==ID_incomplete_struct ||
+                   type.id()==ID_incomplete_union,
+                   "operand 0 of member expression must be struct or union");
 
     const std::string &component_name=
       expr.get_string(ID_component_name);
@@ -1360,7 +1362,8 @@ void value_sett::assign_rec(
 
     const typet &type=ns.follow(lhs.op0().type());
 
-    assert(type.id()==ID_array || type.id()==ID_incomplete_array);
+    DATA_INVARIANT(type.id()==ID_array || type.id()==ID_incomplete_array,
+                   "operand 0 of index expression must be an array");
 
     assign_rec(lhs.op0(), values_rhs, "[]"+suffix, ns, true);
   }
@@ -1373,10 +1376,11 @@ void value_sett::assign_rec(
 
     const typet &type=ns.follow(lhs.op0().type());
 
-    assert(type.id()==ID_struct ||
-           type.id()==ID_union ||
-           type.id()==ID_incomplete_struct ||
-           type.id()==ID_incomplete_union);
+    DATA_INVARIANT(type.id()==ID_struct ||
+                   type.id()==ID_union ||
+                   type.id()==ID_incomplete_struct ||
+                   type.id()==ID_incomplete_union,
+                   "operand 0 of member expression must be struct or union");
 
     assign_rec(
       lhs.op0(), values_rhs, "."+component_name+suffix, ns, add_to_sets);

src/pointer-analysis/value_set_fi.cpp

@@ -412,9 +412,10 @@ void value_set_fit::get_value_set_rec(
 
     const typet &type=ns.follow(expr.op0().type());
 
-    assert(type.id()==ID_array ||
-           type.id()==ID_incomplete_array ||
-           type.id()=="#REF#");
+    DATA_INVARIANT(type.id()==ID_array ||
+                   type.id()==ID_incomplete_array ||
+                   type.id()=="#REF#",
+                   "operand 0 of index expression must be an array");
 
     get_value_set_rec(expr.op0(), dest, "[]"+suffix,
                       original_type, ns, recursion_set);
@@ -429,10 +430,11 @@ void value_set_fit::get_value_set_rec(
     {
       const typet &type=ns.follow(expr.op0().type());
 
-      assert(type.id()==ID_struct ||
-             type.id()==ID_union ||
-             type.id()==ID_incomplete_struct ||
-             type.id()==ID_incomplete_union);
+      DATA_INVARIANT(type.id()==ID_struct ||
+                     type.id()==ID_union ||
+                     type.id()==ID_incomplete_struct ||
+                     type.id()==ID_incomplete_union,
+                     "operand 0 of member expression must be struct or union");
 
       const std::string &component_name=
         expr.get_string(ID_component_name);
@@ -1290,9 +1292,10 @@ void value_set_fit::assign_rec(
 
     const typet &type=ns.follow(lhs.op0().type());
 
-    assert(type.id()==ID_array ||
-           type.id()==ID_incomplete_array ||
-           type.id()=="#REF#");
+    DATA_INVARIANT(type.id()==ID_array ||
+                   type.id()==ID_incomplete_array ||
+                   type.id()=="#REF#",
+                   "operand 0 of index expression must be an array");
 
     assign_rec(lhs.op0(), values_rhs, "[]"+suffix, ns, recursion_set);
   }
@@ -1308,10 +1311,11 @@ void value_set_fit::assign_rec(
 
     const typet &type=ns.follow(lhs.op0().type());
 
-    assert(type.id()==ID_struct ||
-           type.id()==ID_union ||
-           type.id()==ID_incomplete_struct ||
-           type.id()==ID_incomplete_union);
+    DATA_INVARIANT(type.id()==ID_struct ||
+                   type.id()==ID_union ||
+                   type.id()==ID_incomplete_struct ||
+                   type.id()==ID_incomplete_union,
+                   "operand 0 of member expression must be struct or union");
 
     assign_rec(lhs.op0(), values_rhs, "."+component_name+suffix,
                ns, recursion_set);

src/pointer-analysis/value_set_fivr.cpp

@@ -525,9 +525,10 @@ void value_set_fivrt::get_value_set_rec(
 
     const typet &type=ns.follow(expr.op0().type());
 
-    assert(type.id()==ID_array ||
-           type.id()==ID_incomplete_array ||
-           type.id()=="#REF#");
+    DATA_INVARIANT(type.id()==ID_array ||
+                   type.id()==ID_incomplete_array ||
+                   type.id()=="#REF#",
+                   "operand 0 of index expression must be an array");
 
     get_value_set_rec(expr.op0(), dest, "[]"+suffix,
                       original_type, ns, recursion_set);
@@ -542,10 +543,11 @@ void value_set_fivrt::get_value_set_rec(
     {
       const typet &type=ns.follow(expr.op0().type());
 
-      assert(type.id()==ID_struct ||
-             type.id()==ID_union ||
-             type.id()==ID_incomplete_struct ||
-             type.id()==ID_incomplete_union);
+      DATA_INVARIANT(type.id()==ID_struct ||
+                     type.id()==ID_union ||
+                     type.id()==ID_incomplete_struct ||
+                     type.id()==ID_incomplete_union,
+                     "operand 0 of member expression must be struct or union");
 
       const std::string &component_name=
         expr.get_string(ID_component_name);
@@ -1427,9 +1429,10 @@ void value_set_fivrt::assign_rec(
 
     const typet &type=ns.follow(lhs.op0().type());
 
-    assert(type.id()==ID_array ||
-           type.id()==ID_incomplete_array ||
-           type.id()=="#REF#");
+    DATA_INVARIANT(type.id()==ID_array ||
+                   type.id()==ID_incomplete_array ||
+                   type.id()=="#REF#",
+                   "operand 0 of index expression must be an array");
 
     assign_rec(
       lhs.op0(), values_rhs, "[]"+suffix, ns, recursion_set, add_to_sets);
@@ -1446,10 +1449,11 @@ void value_set_fivrt::assign_rec(
 
     const typet &type=ns.follow(lhs.op0().type());
 
-    assert(type.id()==ID_struct ||
-           type.id()==ID_union ||
-           type.id()==ID_incomplete_struct ||
-           type.id()==ID_incomplete_union);
+    DATA_INVARIANT(type.id()==ID_struct ||
+                   type.id()==ID_union ||
+                   type.id()==ID_incomplete_struct ||
+                   type.id()==ID_incomplete_union,
+                   "operand 0 of member expression must be struct or union");
 
     assign_rec(lhs.op0(), values_rhs, "."+component_name+suffix,
                ns, recursion_set, add_to_sets);