#include <util/std_code.h>

Include dependency graph for nondet.h:

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

Typedefs
using	allocate_local_symbolt = std::function< symbol_exprt(const typet &type, std::string)>

typedef std::vector< codet >	alternate_casest

Functions
symbol_exprt	generate_nondet_int (const exprt &min_value_expr, const exprt &max_value_expr, const std::string &basename_prefix, const source_locationt &source_location, allocate_objectst &allocate_objects, code_blockt &instructions)
	Same as generate_nondet_int( const mp_integer &min_value, const mp_integer &max_value, const std::string &name_prefix, const typet &int_type, const irep_idt &mode, const source_locationt &source_location, symbol_table_baset &symbol_table, code_blockt &instructions) except the minimum and maximum values are represented as exprts. More...

symbol_exprt	generate_nondet_int (const exprt &min_value_expr, const exprt &max_value_expr, const std::string &basename_prefix, const source_locationt &source_location, const allocate_local_symbolt &alocate_local_symbol, code_blockt &instructions)

symbol_exprt	generate_nondet_int (const mp_integer &min_value, const mp_integer &max_value, const std::string &basename_prefix, const typet &int_type, const source_locationt &source_location, allocate_objectst &allocate_objects, code_blockt &instructions)
	Gets a fresh nondet choice in range (min_value, max_value). More...

code_blockt	generate_nondet_switch (const irep_idt &name_prefix, const alternate_casest &switch_cases, const typet &int_type, const irep_idt &mode, const source_locationt &source_location, symbol_table_baset &symbol_table)
	Pick nondeterministically between imperative actions 'switch_cases'. More...

Typedef Documentation

◆ allocate_local_symbolt

using allocate_local_symbolt = std::function<symbol_exprt(const typet &type, std::string)>

Definition at line 18 of file nondet.h.

◆ alternate_casest

typedef std::vector<codet> alternate_casest

Definition at line 73 of file nondet.h.

Function Documentation

◆ generate_nondet_int() [1/3]

symbol_exprt generate_nondet_int	(	const exprt &	min_value_expr,
		const exprt &	max_value_expr,
		const std::string &	basename_prefix,
		const source_locationt &	source_location,
		allocate_objectst &	allocate_objects,
		code_blockt &	instructions
	)

Same as generate_nondet_int( const mp_integer &min_value, const mp_integer &max_value, const std::string &name_prefix, const typet &int_type, const irep_idt &mode, const source_locationt &source_location, symbol_table_baset &symbol_table, code_blockt &instructions) except the minimum and maximum values are represented as exprts.

Definition at line 15 of file nondet.cpp.

◆ generate_nondet_int() [2/3]

symbol_exprt generate_nondet_int	(	const exprt &	min_value_expr,
		const exprt &	max_value_expr,
		const std::string &	basename_prefix,
		const source_locationt &	source_location,
		const allocate_local_symbolt &	alocate_local_symbol,
		code_blockt &	instructions
	)

Definition at line 38 of file nondet.cpp.

◆ generate_nondet_int() [3/3]

symbol_exprt generate_nondet_int	(	const mp_integer &	min_value,
		const mp_integer &	max_value,
		const std::string &	basename_prefix,
		const typet &	int_type,
		const source_locationt &	source_location,
		allocate_objectst &	allocate_objects,
		code_blockt &	instructions
	)

Gets a fresh nondet choice in range (min_value, max_value).

GOTO generated resembles:

int_type name_prefix::nondet_int = NONDET(int_type)
ASSUME(name_prefix::nondet_int >= min_value)
ASSUME(name_prefix::nondet_int <= max_value)

Parameters

	min_value	Minimum value (inclusive) of returned int.
	max_value	Maximum value (inclusive) of returned int.
	basename_prefix	Basename prefix for the fresh symbol name generated.
	int_type	The type of the int used to non-deterministically choose one of the switch cases.
	allocate_objects	Handles allocation of new objects.
	source_location	The location to mark the generated int with.
[out]	instructions	Output instructions are written to 'instructions'. These declare, nondet-initialise and range-constrain (with assume statements) a fresh integer.

Returns: Returns a symbol expression for the resulting integer.

Definition at line 72 of file nondet.cpp.

◆ generate_nondet_switch()

code_blockt generate_nondet_switch	(	const irep_idt &	name_prefix,
		const alternate_casest &	switch_cases,
		const typet &	int_type,
		const irep_idt &	mode,
		const source_locationt &	source_location,
		symbol_table_baset &	symbol_table
	)

Pick nondeterministically between imperative actions 'switch_cases'.