Skip to content

Commit 015da34

Browse files
committed
Java bytecode: type checking symbol expressions cannot yield a fresh symbol
java_bytecode_convert_class and java_bytecode_convert_method take care of adding all symbols to the symbol table ahead of type checking. Therefore, typecheck_expr_symbol could never end up in the branch where a symbol was missing. This commit removes this branch.
1 parent 7e81905 commit 015da34

File tree

1 file changed

+7
-43
lines changed

1 file changed

+7
-43
lines changed

jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp

Lines changed: 7 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -69,50 +69,14 @@ void java_bytecode_typecheckt::typecheck_expr_java_new_array(
6969

7070
void java_bytecode_typecheckt::typecheck_expr_symbol(symbol_exprt &expr)
7171
{
72-
irep_idt identifier=expr.get_identifier();
72+
const irep_idt &identifier = expr.get_identifier();
7373

74-
// does it exist already in the destination symbol table?
75-
symbol_tablet::symbolst::const_iterator s_it=
76-
symbol_table.symbols.find(identifier);
74+
// the java_bytecode_convert_class and java_bytecode_convert_method made sure
75+
// "identifier" exists in the symbol table
76+
const symbolt &symbol = symbol_table.lookup_ref(identifier);
7777

78-
if(s_it==symbol_table.symbols.end())
79-
{
80-
PRECONDITION(
81-
has_prefix(id2string(identifier), "java::") ||
82-
has_prefix(id2string(identifier), CPROVER_PREFIX));
83-
84-
// no, create the symbol
85-
symbolt new_symbol;
86-
new_symbol.name=identifier;
87-
new_symbol.type=expr.type();
88-
new_symbol.base_name=expr.get(ID_C_base_name);
89-
new_symbol.pretty_name=id2string(identifier).substr(6, std::string::npos);
90-
new_symbol.mode=ID_java;
91-
new_symbol.is_type=false;
92-
93-
if(new_symbol.type.id()==ID_code)
94-
{
95-
new_symbol.is_lvalue=false;
96-
}
97-
else
98-
{
99-
new_symbol.is_lvalue=true;
100-
}
101-
102-
if(symbol_table.add(new_symbol))
103-
{
104-
error() << "failed to add expression symbol to symbol table" << eom;
105-
throw 0;
106-
}
107-
}
108-
else
109-
{
110-
// yes!
111-
INVARIANT(!s_it->second.is_type, "symbol identifier should not be a type");
78+
INVARIANT(!symbol.is_type, "symbol identifier should not be a type");
11279

113-
const symbolt &symbol=s_it->second;
114-
115-
// type the expression
116-
expr.type()=symbol.type;
117-
}
80+
// type the expression
81+
expr.type() = symbol.type;
11882
}

0 commit comments

Comments
 (0)