CBMC
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 java_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 (const irep_idt &function_identifier, goto_programt &goto_program, const goto_programt::targett &target, symbol_table_baset &symbol_table, message_handlert &message_handler, java_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 (const irep_idt &function_identifier, goto_programt &goto_program, symbol_table_baset &symbol_table, message_handlert &message_handler, const java_object_factory_parameterst &user_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 java_object_factory_parameterst &object_factory_parameters, const irep_idt &mode)
 Converts side_effect_exprt_nondett expressions using java_object_factory. More...
 
void convert_nondet (goto_functionst &goto_functions, symbol_table_baset &symbol_table, message_handlert &message_handler, const java_object_factory_parameterst &object_factory_parameters)
 Converts side_effect_exprt_nondett expressions using java_object_factory. More...
 
void convert_nondet (goto_modelt &goto_model, message_handlert &message_handler, const java_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 ( const irep_idt function_identifier,
goto_programt goto_program,
symbol_table_baset symbol_table,
message_handlert message_handler,
const java_object_factory_parameterst user_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
function_identifierName of the function goto_program.
goto_programThe goto program to modify.
symbol_tableThe global symbol table.
message_handlerHandles logging.
user_object_factory_parametersParameters for the generation of nondet objects.
modeLanguage mode

Definition at line 166 of file convert_java_nondet.cpp.

◆ convert_nondet() [2/4]

void convert_nondet ( goto_functionst goto_functions,
symbol_table_baset symbol_table,
message_handlert message_handler,
const java_object_factory_parameterst object_factory_parameters 
)

Converts side_effect_exprt_nondett expressions using java_object_factory.

For example, NONDET(SomeClass *) may become a nondet choice between a null pointer and a fresh instance of SomeClass, whose fields are in turn nondet initialized in the same way. See java_object_factory.h for details.

Note the code introduced has been freshly goto_convert'd without any passes such as remove_java_new being run. Therefore the caller may need to (re-)run this and other expected GOTO transformations after this pass completes.

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.

◆ convert_nondet() [3/4]

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

Converts side_effect_exprt_nondett expressions using java_object_factory.

For example, NONDET(SomeClass *) may become a nondet choice between a null pointer and a fresh instance of SomeClass, whose fields are in turn nondet initialized in the same way. See java_object_factory.h for details.

Note the code introduced has been freshly goto_convert'd without any passes such as remove_java_new being run. Therefore the caller may need to (re-)run this and other expected GOTO transformations after this pass completes.

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

Definition at line 201 of file convert_java_nondet.cpp.

◆ convert_nondet() [4/4]

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

Definition at line 247 of file convert_java_nondet.cpp.

◆ 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 java_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 41 of file convert_java_nondet.cpp.

◆ insert_nondet_init_code()

static std::pair<goto_programt::targett, bool> insert_nondet_init_code ( const irep_idt function_identifier,
goto_programt goto_program,
const goto_programt::targett target,
symbol_table_baset symbol_table,
message_handlert message_handler,
java_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
function_identifierName of the function containing target.
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 81 of file convert_java_nondet.cpp.

◆ 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 25 of file convert_java_nondet.cpp.