Skip to content

Commit 985baf1

Browse files
Take care of cases where the symbol exists in table diffblue/test-gen#480
In add_string_type, instead of deleting the symbol from the symbol table and then adding one with the same name, we use symbol.move to get a pointer to the existing symbol if it exist or create a new one.
1 parent 2120a44 commit 985baf1

File tree

1 file changed

+12
-13
lines changed

1 file changed

+12
-13
lines changed

src/java_bytecode/java_string_library_preprocess.cpp

+12-13
Original file line numberDiff line numberDiff line change
@@ -260,8 +260,9 @@ typet string_data_type(symbol_tablet symbol_table)
260260
{
261261
symbolt sym=symbol_table.lookup("java::java.lang.String");
262262
typet concrete_type=sym.type;
263-
// TODO: Check that this is indeed the 'length' field.
264-
typet data_type=to_struct_type(concrete_type).components()[2].type();
263+
struct_typet struct_type=to_struct_type(concrete_type);
264+
std::size_t index=struct_type.component_number("data");
265+
typet data_type=struct_type.components()[index].type();
265266
return data_type;
266267
}
267268

@@ -312,17 +313,15 @@ void java_string_library_preprocesst::add_string_type(
312313
array_typet(java_char_type(), infinity_exprt(string_length_type())));
313314
string_type.add_base(symbol_typet("java::java.lang.Object"));
314315

315-
symbolt string_symbol;
316-
string_symbol.name="java::"+id2string(class_name);
317-
string_symbol.base_name=id2string(class_name);
318-
string_symbol.pretty_name=id2string(class_name);
319-
string_symbol.type=string_type;
320-
string_symbol.is_type=true;
321-
322-
// Overwrite any pre-existing symbol in the table, e.g. created by
323-
// a loaded model.
324-
symbol_table.remove(string_symbol.name);
325-
assert(!symbol_table.add(string_symbol));
316+
std::string name="java::"+id2string(class_name);
317+
symbolt tmp_string_symbol;
318+
tmp_string_symbol.name=name;
319+
symbolt *string_symbol;
320+
symbol_table.move(tmp_string_symbol, string_symbol);
321+
string_symbol->base_name=id2string(class_name);
322+
string_symbol->pretty_name=id2string(class_name);
323+
string_symbol->type=string_type;
324+
string_symbol->is_type=true;
326325
}
327326

328327
/*******************************************************************\

0 commit comments

Comments
 (0)