convert_java_nondet.h File Reference

Convert side_effect_expr_nondett expressions using java_object_factory. More...

#include <util/irep.h>

Include dependency graph for convert_java_nondet.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions
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 &, message_handlert &, const java_object_factory_parameterst &object_factory_parameters)
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...

Detailed Description

Convert side_effect_expr_nondett expressions using java_object_factory.

Definition in file convert_java_nondet.h.

Function Documentation

convert_nondet() [1/3]

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_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 217 of file convert_java_nondet.cpp.

convert_nondet() [2/3]

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

function	goto program to modify
message_handler	For error logging.
object_factory_parameters	Parameters for the generation of nondet objects.
mode	Mode for newly created symbols

Definition at line 200 of file convert_java_nondet.cpp.

convert_nondet() [3/3]

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

Definition at line 246 of file convert_java_nondet.cpp.