cprover
|
Public Member Functions | |
java_simple_method_stubst (symbol_table_baset &_symbol_table, bool _assume_non_null, const object_factory_parameterst &_object_factory_parameters, message_handlert &_message_handler) | |
void | create_method_stub_at (const typet &expected_type, const exprt &ptr, const source_locationt &loc, const irep_idt &function_id, code_blockt &parent_block, unsigned insert_before_index, bool is_constructor, bool update_in_place) |
Nondet-initialize an object, including allocating referees for reference fields and nondet-initialising those recursively. More... | |
void | create_method_stub (symbolt &symbol) |
Replaces sym's value with an opaque method stub. More... | |
void | check_method_stub (const irep_idt &) |
Replaces sym with a function stub per the function above if it is of suitable type. More... | |
Protected Attributes | |
symbol_table_baset & | symbol_table |
bool | assume_non_null |
const object_factory_parameterst & | object_factory_parameters |
message_handlert & | message_handler |
Definition at line 23 of file simple_method_stubbing.cpp.
|
inline |
Definition at line 26 of file simple_method_stubbing.cpp.
void java_simple_method_stubst::check_method_stub | ( | const irep_idt & | symname | ) |
Replaces sym
with a function stub per the function above if it is of suitable type.
symname | Symbol name to consider stubbing |
Definition at line 233 of file simple_method_stubbing.cpp.
References create_method_stub(), symbol_table_baset::get_writeable(), irept::id(), symbolt::is_type, symbol_table_baset::lookup(), symbolt::name, symbol_table, symbolt::type, and symbolt::value.
Referenced by java_generate_simple_method_stub(), and java_generate_simple_method_stubs().
void java_simple_method_stubst::create_method_stub | ( | symbolt & | symbol | ) |
Replaces sym's value with an opaque method stub.
If sym is a constructor function this nondet-initializes *this
using the function above; otherwise it generates a return value using a similar method.
symbol | Function symbol to stub |
Definition at line 145 of file simple_method_stubbing.cpp.
References exprt::add_source_location(), assume_non_null, exprt::copy_to_operands(), create_method_stub_at(), gen_nondet_init(), get_fresh_aux_symbol(), code_typet::get_is_constructor(), irept::id(), id2string(), is_constructor(), LOCAL, object_factory_parameterst::max_nonnull_tree_depth, symbolt::name, NO_UPDATE_IN_PLACE, object_factory_parameters, code_typet::parameters(), code_typet::return_type(), source_locationt::set_function(), symbolt::symbol_expr(), symbol_table, to_code_type(), symbolt::type, and symbolt::value.
Referenced by check_method_stub().
void java_simple_method_stubst::create_method_stub_at | ( | const typet & | expected_type, |
const exprt & | ptr, | ||
const source_locationt & | loc, | ||
const irep_idt & | function_id, | ||
code_blockt & | parent_block, | ||
unsigned | insert_before_index, | ||
bool | is_constructor, | ||
bool | update_in_place | ||
) |
Nondet-initialize an object, including allocating referees for reference fields and nondet-initialising those recursively.
Reference fields are nondeterministically assigned either a fresh object or null; arrays are additionally nondeterministically assigned between 0 and max_nondet_array_length
members.
expected_type | the expected actual type of ptr . We will cast ptr to this type and initialize assuming the actual referee has this type. | |
ptr | pointer to the memory to initialize | |
loc | source location to set for the opaque method stub | |
[out] | parent_block | The parent block in which the new instructions will be added. |
insert_before_index | The position in which the new instructions will be added. | |
is_constructor | true if we're initialising the this pointer of a constructor. In this case the target's class identifier has been set and should not be overridden. | |
update_in_place | Whether to generate the nondet in place or not. |
Definition at line 77 of file simple_method_stubbing.cpp.
References assume_non_null, DYNAMIC, object_factory_parameterst::function_id, gen_nondet_init(), irept::id(), INVARIANT_WITH_IREP, is_constructor(), loc, make_clean_pointer_cast(), object_factory_parameterst::max_nonnull_tree_depth, MUST_UPDATE_IN_PLACE, NO_UPDATE_IN_PLACE, object_factory_parameters, exprt::operands(), typet::subtype(), symbol_table, and to_pointer_type().
Referenced by create_method_stub().
|
protected |
Definition at line 54 of file simple_method_stubbing.cpp.
Referenced by create_method_stub(), and create_method_stub_at().
|
protected |
Definition at line 56 of file simple_method_stubbing.cpp.
|
protected |
Definition at line 55 of file simple_method_stubbing.cpp.
Referenced by create_method_stub(), and create_method_stub_at().
|
protected |
Definition at line 53 of file simple_method_stubbing.cpp.
Referenced by check_method_stub(), create_method_stub(), and create_method_stub_at().