cprover
|
Convert side_effect_expr_nondett expressions. More...
#include "convert_java_nondet.h"
#include <goto-programs/goto_convert.h>
#include <goto-programs/goto_model.h>
#include <goto-programs/remove_skip.h>
#include <util/fresh_symbol.h>
#include <util/irep_ids.h>
#include <memory>
#include "java_object_factory.h"
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) |
Convert side_effect_expr_nondett expressions.
Definition in file convert_java_nondet.cpp.
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.
goto_program | The goto program to modify. |
symbol_table | The global symbol table. |
message_handler | Handles logging. |
max_nondet_array_length | Maximum 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().
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.
function | goto program to modify |
message_handler | For error logging. |
object_factory_parameters | Parameters 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.
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.
goto_functions | The set of goto programs to modify. |
symbol_table | The symbol table to query/update. |
message_handler | For error logging. |
object_factory_parameters | Parameters 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().
void convert_nondet | ( | goto_modelt & | goto_model, |
message_handlert & | message_handler, | ||
const object_factory_parameterst & | object_factory_parameters | ||
) |
Definition at line 187 of file convert_java_nondet.cpp.
References convert_nondet(), goto_modelt::goto_functions, message_handler, and goto_modelt::symbol_table.
|
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.
goto_program | The goto program to modify. |
target | One of the steps in that goto program. |
symbol_table | The global symbol table. |
message_handler | Handles logging. |
max_nondet_array_length | Maximum size of new nondet arrays. |
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().