Skip to content

Commit a8bcdb5

Browse files
Replace asserts by invariants
1 parent 2f18e98 commit a8bcdb5

File tree

1 file changed

+9
-12
lines changed

1 file changed

+9
-12
lines changed

src/java_bytecode/java_bytecode_typecheck_type.cpp

Lines changed: 9 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -12,24 +12,20 @@ Author: Daniel Kroening, [email protected]
1212
#include "java_bytecode_typecheck.h"
1313

1414
#include <util/std_types.h>
15+
#include <util/invariant.h>
1516

1617
void java_bytecode_typecheckt::typecheck_type(typet &type)
1718
{
1819
if(type.id()==ID_symbol)
1920
{
2021
irep_idt identifier=to_symbol_type(type).get_identifier();
2122

22-
symbol_tablet::symbolst::const_iterator s_it=
23-
symbol_table.symbols.find(identifier);
24-
25-
// must exist already in the symbol table
26-
if(s_it==symbol_table.symbols.end())
27-
{
28-
error() << "failed to find type symbol "<< identifier << eom;
29-
throw 0;
30-
}
31-
32-
assert(s_it->second.is_type);
23+
const auto type_symbol = symbol_table.lookup(identifier);
24+
DATA_INVARIANT(
25+
type_symbol, "symbol " + id2string(identifier) + " must exist already");
26+
DATA_INVARIANT(
27+
type_symbol->is_type,
28+
"symbol " + id2string(identifier) + " must be a type");
3329
}
3430
else if(type.id()==ID_pointer)
3531
{
@@ -55,7 +51,8 @@ void java_bytecode_typecheckt::typecheck_type(typet &type)
5551

5652
void java_bytecode_typecheckt::typecheck_type_symbol(symbolt &symbol)
5753
{
58-
assert(symbol.is_type);
54+
DATA_INVARIANT(
55+
symbol.is_type, "symbol " + id2string(symbol.name) + " must exist already");
5956

6057
typecheck_type(symbol.type);
6158
}

0 commit comments

Comments
 (0)