Inheritance diagram for java_object_factory_parameterst:

Collaboration diagram for java_object_factory_parameterst:

Public Member Functions
	java_object_factory_parameterst ()

	java_object_factory_parameterst (const optionst &options)

void	set (const optionst &)
	Assigns the parameters from given options.

Public Member Functions inherited from object_factory_parameterst
	object_factory_parameterst ()

	object_factory_parameterst (const optionst &options)

virtual	~object_factory_parameterst ()=default

void	set (const optionst &)
	Assigns the parameters from given options.

Public Attributes
interval_uniont	assume_inputs_interval = interval_uniont::all_integers()
	Force numerical primitive inputs to fall within the interval.

bool	assume_inputs_integral
	Force double and float inputs to be integral.

Public Attributes inherited from object_factory_parameterst
size_t	max_nondet_array_length = 5
	Maximum value for the non-deterministically-chosen length of an array.

size_t	max_nondet_string_length = MAX_CONCRETE_STRING_SIZE - 1
	Maximum value for the non-deterministically-chosen length of a string.

size_t	min_nondet_string_length = 0
	Minimum value for the non-deterministically-chosen length of a string.

size_t	max_nondet_tree_depth = 5
	Maximum depth of pointer chains (that contain recursion) in the nondet generated input objects.

size_t	min_null_tree_depth = 0
	To force a certain depth of non-null objects.

bool	string_printable = false
	Force string content to be ASCII printable characters when set to true.

std::list< std::string >	string_input_values
	Force one of finitely many explicitly given input strings.

irep_idt	function_id
	Function id, used as a prefix for identifiers of temporaries.

Detailed Description

Constructor & Destructor Documentation

java_object_factory_parameterst::java_object_factory_parameterst ( )

inline

java_object_factory_parameterst::java_object_factory_parameterst ( const optionst & options )

inlineexplicit

void java_object_factory_parameterst::set ( const optionst & options )

Assigns the parameters from given options.

bool java_object_factory_parameterst::assume_inputs_integral

Force double and float inputs to be integral.

interval_uniont java_object_factory_parameterst::assume_inputs_interval = interval_uniont::all_integers()

Force numerical primitive inputs to fall within the interval.

The documentation for this struct was generated from the following files:

/home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/java_object_factory_parameters.h
/home/runner/work/cbmc/cbmc/jbmc/src/java_bytecode/java_object_factory_parameters.cpp