cprover
convert_java_nondet.cpp File Reference

Convert side_effect_expr_nondett expressions. More...

Include dependency graph for convert_java_nondet.cpp:

Go to the source code of this file.

Functions

static goto_programt::targett insert_nondet_init_code (goto_programt &goto_program, const goto_programt::targett &target, symbol_table_baset &symbol_table, message_handlert &message_handler, object_factory_parameterst object_factory_parameters, const irep_idt &mode)
 Checks an instruction to see whether it contains an assignment from side_effect_expr_nondet. More...
 
void convert_nondet (goto_programt &goto_program, symbol_table_baset &symbol_table, message_handlert &message_handler, const object_factory_parameterst &object_factory_parameters, const irep_idt &mode)
 For each instruction in the goto program, checks if it is an assignment from nondet and replaces it with the appropriate composite initialization code if so. More...
 
void convert_nondet (goto_model_functiont &function, message_handlert &message_handler, const object_factory_parameterst &object_factory_parameters, const irep_idt &mode)
 Replace calls to nondet library functions with an internal nondet representation. More...
 
void convert_nondet (goto_functionst &goto_functions, symbol_table_baset &symbol_table, message_handlert &message_handler, const object_factory_parameterst &object_factory_parameters)
 Replace calls to nondet library functions with an internal nondet representation. More...
 
void convert_nondet (goto_modelt &goto_model, message_handlert &message_handler, const object_factory_parameterst &object_factory_parameters)
 

Detailed Description

Convert side_effect_expr_nondett expressions.

Definition in file convert_java_nondet.cpp.

Function Documentation

◆ convert_nondet() [1/4]

void convert_nondet ( goto_programt goto_program,
symbol_table_baset symbol_table,
message_handlert message_handler,
const object_factory_parameterst object_factory_parameters,
const irep_idt mode 
)

For each instruction in the goto program, checks if it is an assignment from nondet and replaces it with the appropriate composite initialization code if so.

Parameters
goto_programThe goto program to modify.
symbol_tableThe global symbol table.
message_handlerHandles logging.
max_nondet_array_lengthMaximum size of new nondet arrays.

Definition at line 118 of file convert_java_nondet.cpp.

References goto_program, insert_nondet_init_code(), goto_programt::instructions, and message_handler.

Referenced by convert_nondet(), and jbmc_parse_optionst::process_goto_function().

◆ convert_nondet() [2/4]

void convert_nondet ( goto_model_functiont function,
message_handlert message_handler,
const object_factory_parameterst object_factory_parameters,
const irep_idt mode 
)

Replace calls to nondet library functions with an internal nondet representation.

Parameters
functiongoto program to modify
message_handlerFor error logging.
object_factory_parametersParameters for the generation of nondet objects.

Definition at line 139 of file convert_java_nondet.cpp.

References convert_nondet(), object_factory_parameterst::function_id, and message_handler.

◆ convert_nondet() [3/4]

void convert_nondet ( goto_functionst ,
symbol_table_baset ,
message_handlert ,
const object_factory_parameterst object_factory_parameters 
)

Replace calls to nondet library functions with an internal nondet representation.

Parameters
goto_functionsThe set of goto programs to modify.
symbol_tableThe symbol table to query/update.
message_handlerFor error logging.
object_factory_parametersParameters for the generation of nondet objects.

Definition at line 157 of file convert_java_nondet.cpp.

References goto_functionst::compute_location_numbers(), convert_nondet(), object_factory_parameterst::function_id, goto_functionst::function_map, namespacet::lookup(), message_handler, symbolt::mode, and remove_skip().

◆ convert_nondet() [4/4]

void convert_nondet ( goto_modelt goto_model,
message_handlert message_handler,
const object_factory_parameterst object_factory_parameters 
)

◆ insert_nondet_init_code()

static goto_programt::targett insert_nondet_init_code ( goto_programt goto_program,
const goto_programt::targett target,
symbol_table_baset symbol_table,
message_handlert message_handler,
object_factory_parameterst  object_factory_parameters,
const irep_idt mode 
)
static

Checks an instruction to see whether it contains an assignment from side_effect_expr_nondet.

If so, replaces the instruction with a range of instructions to properly nondet-initialize the lhs.

Parameters
goto_programThe goto program to modify.
targetOne of the steps in that goto program.
symbol_tableThe global symbol table.
message_handlerHandles logging.
max_nondet_array_lengthMaximum size of new nondet arrays.
Returns
The next instruction to process with this function.

Definition at line 34 of file convert_java_nondet.cpp.

References goto_programt::destructive_insert(), DYNAMIC, gen_nondet_init(), side_effect_expr_nondett::get_nullable(), goto_convert(), goto_program, object_factory_parameterst::max_nonnull_tree_depth, message_handler, NO_UPDATE_IN_PLACE, to_code_assign(), to_side_effect_expr(), to_side_effect_expr_nondet(), and goto_programt::update().

Referenced by convert_nondet().