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 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) |
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. |
object_factory_parameters | Parameters for the generation of nondet objects. |
mode | Language 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().
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 200 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 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().
void convert_nondet | ( | goto_modelt & | goto_model, |
message_handlert & | message_handler, | ||
const object_factory_parameterst & | object_factory_parameters | ||
) |
Definition at line 248 of file convert_java_nondet.cpp.
References convert_nondet(), goto_modelt::goto_functions, message_handler, and goto_modelt::symbol_table.
|
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().
|
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. |
object_factory_parameters | Parameters for the generation of nondet objects. |
mode | Language mode |
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().
|
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().