Skip to content

Commit 9a896f9

Browse files
Replace asserts by invariants
1 parent e4cf694 commit 9a896f9

File tree

1 file changed

+9
-12
lines changed

1 file changed

+9
-12
lines changed

src/java_bytecode/java_bytecode_typecheck_type.cpp

+9-12
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include "java_bytecode_typecheck.h"
1313

14+
#include <util/invariant.h>
1415
#include <util/std_types.h>
1516

1617
void java_bytecode_typecheckt::typecheck_type(typet &type)
@@ -19,17 +20,12 @@ void java_bytecode_typecheckt::typecheck_type(typet &type)
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+
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 be a type");
5956

6057
symbol.mode = ID_java;
6158
typecheck_type(symbol.type);

0 commit comments

Comments
 (0)