Skip to content

Replace fresh_java_symbol in object factory #4457

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Apr 2, 2019
Merged

Replace fresh_java_symbol in object factory #4457

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 14 additions & 14 deletions jbmc/src/java_bytecode/java_object_factory.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -335,6 +335,8 @@ class recursion_set_entryt
/// \param symbol_table: the symbol table
/// \param printable: if true, the nondet string must consist of printable
/// characters only
/// \param allocate_objects: manages memory allocation and keeps track of the
/// newly created symbols
///
/// The code produced is of the form:
/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Expand Down Expand Up @@ -366,7 +368,8 @@ void initialize_nondet_string_fields(
const source_locationt &loc,
const irep_idt &function_id,
symbol_table_baset &symbol_table,
bool printable)
bool printable,
allocate_objectst &allocate_objects)
{
PRECONDITION(
java_string_library_preprocesst
Expand Down Expand Up @@ -402,11 +405,10 @@ void initialize_nondet_string_fields(

/// \todo Refactor with make_nondet_string_expr
// length_expr = nondet(int);
const symbolt length_sym = fresh_java_symbol(
java_int_type(), "tmp_object_factory", loc, function_id, symbol_table);
const symbol_exprt length_expr = length_sym.symbol_expr();
const symbol_exprt length_expr =
allocate_objects.allocate_automatic_local_object(
java_int_type(), "tmp_object_factory");
const side_effect_expr_nondett nondet_length(length_expr.type(), loc);
code.add(code_declt(length_expr));
code.add(code_assignt(length_expr, nondet_length));

// assume (length_expr >= min_nondet_string_length);
Expand Down Expand Up @@ -709,17 +711,14 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init(
size_t depth,
const source_locationt &location)
{
symbolt new_symbol = fresh_java_symbol(
replacement_pointer,
"tmp_object_factory",
location,
object_factory_parameters.function_id,
symbol_table);
const symbol_exprt new_symbol_expr =
allocate_objects.allocate_automatic_local_object(
replacement_pointer, "tmp_object_factory");

// Generate a new object into this new symbol
gen_nondet_init(
assignments,
new_symbol.symbol_expr(),
new_symbol_expr,
false, // is_sub
"", // class_identifier
false, // skip_classid
Expand All @@ -729,7 +728,7 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init(
update_in_placet::NO_UPDATE_IN_PLACE,
location);

return new_symbol.symbol_expr();
return new_symbol_expr;
}

/// Creates an alternate_casest vector in which each item contains an
Expand Down Expand Up @@ -874,7 +873,8 @@ void java_object_factoryt::gen_nondet_struct_init(
location,
object_factory_parameters.function_id,
symbol_table,
object_factory_parameters.string_printable);
object_factory_parameters.string_printable,
allocate_objects);
}

assignments.add(code_assignt(expr, *initial_object));
Expand Down