java_simple_method_stubst Class Reference

Collaboration diagram for java_simple_method_stubst:

Public Member Functions
	java_simple_method_stubst (symbol_table_baset &_symbol_table, bool _assume_non_null, const java_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.
void	create_method_stub (symbolt &symbol)
	Replaces sym's value with an opaque method stub.
void	check_method_stub (const irep_idt &)
	Replaces sym with a function stub per the function above if it is of suitable type.

Protected Attributes
symbol_table_baset &	symbol_table
bool	assume_non_null
const java_object_factory_parameterst &	object_factory_parameters
message_handlert &	message_handler

Detailed Description

Definition at line 25 of file simple_method_stubbing.cpp.

Constructor & Destructor Documentation

java_simple_method_stubst()

java_simple_method_stubst::java_simple_method_stubst ( symbol_table_baset & _symbol_table, bool _assume_non_null, const java_object_factory_parameterst & _object_factory_parameters, message_handlert & _message_handler )

inline

Definition at line 28 of file simple_method_stubbing.cpp.

Member Function Documentation

check_method_stub()

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.

Parameters

symname

Symbol name to consider stubbing

Definition at line 253 of file simple_method_stubbing.cpp.

create_method_stub()

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.

Parameters

symbol

Function symbol to stub

Definition at line 148 of file simple_method_stubbing.cpp.

create_method_stub_at()

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.

Parameters

	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
	function_id	name of the function we're generated stub code for; used to ensure any generated temporaries are created in the correct scope.
[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 81 of file simple_method_stubbing.cpp.

Member Data Documentation

assume_non_null

bool java_simple_method_stubst::assume_non_null

protected

Definition at line 56 of file simple_method_stubbing.cpp.

message_handler

message_handlert& java_simple_method_stubst::message_handler

protected

Definition at line 58 of file simple_method_stubbing.cpp.

object_factory_parameters

const java_object_factory_parameterst& java_simple_method_stubst::object_factory_parameters

protected

Definition at line 57 of file simple_method_stubbing.cpp.

symbol_table

symbol_table_baset& java_simple_method_stubst::symbol_table

protected

Definition at line 55 of file simple_method_stubbing.cpp.

---

The documentation for this class was generated from the following file:

• /builddir/build/BUILD/cbmc-6.9.0-build/cbmc-cbmc-6.9.0/jbmc/src/java_bytecode/simple_method_stubbing.cpp