convert_java_nondet.h File Reference

Convert side_effect_expr_nondett expressions. More...

#include <cstddef>
#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 &, symbol_table_baset &, message_handlert &, const object_factory_parameterst &object_factory_parameters)
	Replace calls to nondet library functions with an internal nondet representation. More...
void	convert_nondet (goto_modelt &, message_handlert &, const object_factory_parameterst &object_factory_parameters)
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...

Detailed Description

Convert side_effect_expr_nondett expressions.

Definition in file convert_java_nondet.h.

Function Documentation

convert_nondet() [1/3]

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.

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 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().

convert_nondet() [2/3]

void convert_nondet	(	goto_modelt &	,
		message_handlert &	,
		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.

convert_nondet() [3/3]

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.

Parameters

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.