Merge pull request #1505 from smowton/smowton/1420-fragments/invariants

Java bytecode typecheck: assert -> invariant

Author: smowton

src/java_bytecode/java_bytecode_typecheck_expr.cpp

@@ -58,15 +58,15 @@ void java_bytecode_typecheckt::typecheck_expr(exprt &expr)
 
 void java_bytecode_typecheckt::typecheck_expr_java_new(side_effect_exprt &expr)
 {
-  assert(expr.operands().empty());
+  PRECONDITION(expr.operands().empty());
   typet &type=expr.type();
   typecheck_type(type);
 }
 
 void java_bytecode_typecheckt::typecheck_expr_java_new_array(
   side_effect_exprt &expr)
 {
-  assert(expr.operands().size()>=1); // one per dimension
+  PRECONDITION(expr.operands().size()>=1); // one per dimension
   typet &type=expr.type();
   typecheck_type(type);
 }
@@ -225,7 +225,7 @@ void java_bytecode_typecheckt::typecheck_expr_symbol(symbol_exprt &expr)
 
   if(s_it==symbol_table.symbols.end())
   {
-    assert(has_prefix(id2string(identifier), "java::"));
+    PRECONDITION(has_prefix(id2string(identifier), "java::"));
 
     // no, create the symbol
     symbolt new_symbol;
@@ -254,7 +254,7 @@ void java_bytecode_typecheckt::typecheck_expr_symbol(symbol_exprt &expr)
   else
   {
     // yes!
-    assert(!s_it->second.is_type);
+    INVARIANT(!s_it->second.is_type, "symbol identifier should not be a type");
 
     const symbolt &symbol=s_it->second;