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 bool is_nondet_pointer (exprt expr)
 Returns true if expr is a nondet pointer that isn't a function pointer or a void* pointer as these can be meaningfully non-det initialized. More...
 
static goto_programt get_gen_nondet_init_instructions (const symbol_exprt &aux_symbol_expr, const source_locationt &source_loc, symbol_table_baset &symbol_table, message_handlert &message_handler, const object_factory_parameterst &object_factory_parameters, const irep_idt &mode)
 Populate instructions with goto instructions to nondet init aux_symbol_expr More...
 
static std::pair< goto_programt::targett, bool > 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.
object_factory_parametersParameters for the generation of nondet objects.
modeLanguage mode

Definition at line 171 of file convert_java_nondet.cpp.

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

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 200 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 218 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 
)

◆ get_gen_nondet_init_instructions()

static goto_programt get_gen_nondet_init_instructions ( const symbol_exprt aux_symbol_expr,
const source_locationt source_loc,
symbol_table_baset symbol_table,
message_handlert message_handler,
const object_factory_parameterst object_factory_parameters,
const irep_idt mode 
)
static

Populate instructions with goto instructions to nondet init aux_symbol_expr

Definition at line 42 of file convert_java_nondet.cpp.

References DYNAMIC, gen_nondet_init(), goto_convert(), message_handler, and NO_UPDATE_IN_PLACE.

Referenced by insert_nondet_init_code().

◆ insert_nondet_init_code()

static std::pair<goto_programt::targett, bool> 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.
object_factory_parametersParameters for the generation of nondet objects.
modeLanguage mode
Returns
The next instruction to process with this function and a boolean indicating whether any changes were made to the goto program.

Definition at line 80 of file convert_java_nondet.cpp.

References goto_programt::destructive_insert(), get_fresh_aux_symbol(), goto_programt::get_function_id(), get_gen_nondet_init_instructions(), goto_program, id2string(), goto_programt::insert_after(), goto_programt::insert_before_swap(), is_nondet_pointer(), goto_programt::instructiont::make_decl(), object_factory_parameterst::max_nonnull_tree_depth, message_handler, exprt::operands(), goto_programt::instructiont::source_location, and to_side_effect_expr_nondet().

Referenced by convert_nondet().

◆ is_nondet_pointer()

static bool is_nondet_pointer ( exprt  expr)
static

Returns true if expr is a nondet pointer that isn't a function pointer or a void* pointer as these can be meaningfully non-det initialized.

Definition at line 27 of file convert_java_nondet.cpp.

References can_cast_expr< side_effect_expr_nondett >(), irept::id(), typet::subtype(), and exprt::type().

Referenced by insert_nondet_init_code().