From 10b5c8e3c7a92c330dcb904a624daa2ad3c978fa Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 26 Sep 2017 16:09:25 +0100 Subject: [PATCH] [java-bytecode/typecheck] Style: Changing assertions in preconditions (or invariant) --- src/java_bytecode/java_bytecode_typecheck_expr.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/java_bytecode/java_bytecode_typecheck_expr.cpp b/src/java_bytecode/java_bytecode_typecheck_expr.cpp index e5b4d0fe572..3c2b0b96fc6 100644 --- a/src/java_bytecode/java_bytecode_typecheck_expr.cpp +++ b/src/java_bytecode/java_bytecode_typecheck_expr.cpp @@ -58,7 +58,7 @@ 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); } @@ -66,7 +66,7 @@ void java_bytecode_typecheckt::typecheck_expr_java_new(side_effect_exprt &expr) 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;