avoid assert()

Author: Daniel Kroening

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1633,7 +1633,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
       const typecast_exprt pointer(op[0], java_array_type(statement[0]));
 
       dereference_exprt array(pointer, pointer.type().subtype());
-      assert(pointer.type().subtype().id() == ID_symbol_type);
+      PRECONDITION(pointer.type().subtype().id() == ID_symbol_type);
       array.set(ID_java_member_access, true);
 
       const member_exprt length(array, "length", java_int_type());

src/ansi-c/c_typecheck_initializer.cpp

@@ -492,7 +492,7 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
 
     const typet &type=designator.back().subtype;
     const typet &full_type=follow(type);
-    assert(full_type.id() != ID_symbol_type);
+    CHECK_RETURN(full_type.id() != ID_symbol_type);
 
     // do we initialize a scalar?
     if(full_type.id()!=ID_struct &&

src/goto-instrument/goto_program2code.cpp

@@ -1861,7 +1861,8 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
     if(no_typecast)
       return;
 
-    assert(expr.type().id() == ID_symbol_type);
+    DATA_INVARIANT(expr.type().id() == ID_symbol_type,
+                   "type of union/struct expressions");
 
     const typet &t=expr.type();