Skip to content

Java object factory: pass function ID to factory routine #4184

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
Feb 14, 2019
Merged

Java object factory: pass function ID to factory routine #4184

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
16 changes: 8 additions & 8 deletions jbmc/src/java_bytecode/convert_java_nondet.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -160,17 +160,21 @@ static std::pair<goto_programt::targett, bool> insert_nondet_init_code(
/// \param goto_program: The goto program to modify.
/// \param symbol_table: The global symbol table.
/// \param message_handler: Handles logging.
/// \param object_factory_parameters: Parameters for the generation of nondet
/// objects.
/// \param user_object_factory_parameters: Parameters for the generation of
/// nondet objects.
/// \param mode: Language mode
void convert_nondet(
const irep_idt &function_identifier,
goto_programt &goto_program,
symbol_table_baset &symbol_table,
message_handlert &message_handler,
const java_object_factory_parameterst &object_factory_parameters,
const java_object_factory_parameterst &user_object_factory_parameters,
const irep_idt &mode)
{
java_object_factory_parameterst object_factory_parameters =
user_object_factory_parameters;
object_factory_parameters.function_id = function_identifier;

bool changed = false;
auto instruction_iterator = goto_program.instructions.begin();

Expand Down Expand Up @@ -200,14 +204,12 @@ void convert_nondet(
const java_object_factory_parameterst &object_factory_parameters,
const irep_idt &mode)
{
java_object_factory_parameterst parameters = object_factory_parameters;
parameters.function_id = function.get_function_id();
convert_nondet(
function.get_function_id(),
function.get_goto_function().body,
function.get_symbol_table(),
message_handler,
parameters,
object_factory_parameters,
mode);

function.compute_location_numbers();
Expand All @@ -227,8 +229,6 @@ void convert_nondet(

if(symbol.mode==ID_java)
{
java_object_factory_parameterst parameters = object_factory_parameters;
parameters.function_id = f_it.first;
convert_nondet(
f_it.first,
f_it.second.body,
Expand Down