Collaboration diagram for state_encodingt:

Public Member Functions
	state_encodingt (const goto_modelt &__goto_model)

void	operator() (const goto_functionst::function_mapt::const_iterator, encoding_targett &)

void	encode (const goto_functiont &, const irep_idt function_identifier, const std::string &state_prefix, const std::vector< irep_idt > &call_stack, const std::string &annotation, const symbol_exprt &entry_state, const exprt &return_lhs, encoding_targett &)

	state_encodingt (const goto_functionst &__goto_functions)

void	operator() (const goto_functionst::function_mapt::const_iterator, encoding_targett &)

void	encode (const goto_functiont &, const std::string &state_prefix, const std::string &annotation, const symbol_exprt &entry_state, const exprt &return_lhs, encoding_targett &)

Protected Types
using	loct = goto_programt::const_targett

using	incomingt = std::map< loct, std::vector< loct >, goto_programt::target_less_than >

using	loct = goto_programt::const_targett

using	incomingt = std::map< loct, std::vector< loct >, goto_programt::target_less_than >

Protected Member Functions
symbol_exprt	out_state_expr (loct) const

symbol_exprt	state_expr_with_suffix (loct, const std::string &suffix) const

symbol_exprt	out_state_expr (loct, bool taken) const

symbol_exprt	in_state_expr (loct) const

std::vector< symbol_exprt >	incoming_symbols (loct) const

exprt	evaluate_expr (loct, const exprt &, const exprt &) const

exprt	evaluate_expr_rec (loct, const exprt &, const exprt &, const std::unordered_set< symbol_exprt, irep_hash > &) const

exprt	replace_nondet_rec (loct, const exprt &, std::vector< symbol_exprt > &nondet_symbols) const

exprt	evaluate_expr (loct, const exprt &) const

exprt	address_rec (loct, const exprt &, exprt) const

exprt	forall_states_expr (loct, exprt) const

exprt	forall_states_expr (loct, exprt, exprt) const

void	setup_incoming (const goto_functiont &)

exprt	assignment_constraint (loct, exprt lhs, exprt rhs) const

exprt	assignment_constraint_rec (loct, exprt state, exprt lhs, exprt rhs, std::vector< symbol_exprt > &nondet_symbols) const

void	function_call (goto_programt::const_targett, encoding_targett &)

void	function_call_symbol (goto_programt::const_targett, encoding_targett &)

symbol_exprt	out_state_expr (loct) const

symbol_exprt	state_expr_with_suffix (loct, const std::string &suffix) const

symbol_exprt	out_state_expr (loct, bool taken) const

symbol_exprt	in_state_expr (loct) const

std::vector< symbol_exprt >	incoming_symbols (loct) const

exprt	evaluate_expr (loct, const exprt &, const exprt &) const

exprt	evaluate_expr_rec (loct, const exprt &, const exprt &, const std::unordered_set< symbol_exprt, irep_hash > &) const

exprt	replace_nondet_rec (loct, const exprt &, std::vector< symbol_exprt > &nondet_symbols) const

exprt	evaluate_expr (loct, const exprt &) const

exprt	address_rec (loct, const exprt &, exprt) const

exprt	forall_states_expr (loct, exprt) const

exprt	forall_states_expr (loct, exprt, exprt) const

void	setup_incoming (const goto_functiont &)

exprt	assignment_constraint (loct, exprt lhs, exprt rhs) const

void	function_call (goto_programt::const_targett, encoding_targett &)

void	function_call_symbol (goto_programt::const_targett, encoding_targett &)

Static Protected Member Functions
static exprt	state_lambda_expr (exprt)

static symbol_exprt	va_args (irep_idt function)

static exprt	state_lambda_expr (exprt)

Protected Attributes
const goto_modelt &	goto_model

irep_idt	function_identifier

std::string	state_prefix

std::string	annotation

std::vector< irep_idt >	call_stack

loct	first_loc

symbol_exprt	entry_state = symbol_exprt(irep_idt(), typet())

exprt	return_lhs = nil_exprt()

incomingt	incoming

const goto_functionst &	goto_functions

Detailed Description

Definition at line 32 of file state_encoding.cpp.

Member Typedef Documentation

◆ incomingt [1/2]

using state_encodingt::incomingt = std::map<loct, std::vector<loct>, goto_programt::target_less_than>

protected

Definition at line 96 of file state_encoding.cpp.

◆ incomingt [2/2]

using state_encodingt::incomingt = std::map<loct, std::vector<loct>, goto_programt::target_less_than>

protected

Definition at line 392 of file horn_encoding.cpp.

◆ loct [1/2]

using state_encodingt::loct = goto_programt::const_targett

protected

Definition at line 55 of file state_encoding.cpp.

◆ loct [2/2]

using state_encodingt::loct = goto_programt::const_targett

protected

Definition at line 359 of file horn_encoding.cpp.

Constructor & Destructor Documentation

◆ state_encodingt() [1/2]

state_encodingt::state_encodingt ( const goto_modelt & __goto_model )

inlineexplicit

Definition at line 35 of file state_encoding.cpp.

◆ state_encodingt() [2/2]

state_encodingt::state_encodingt ( const goto_functionst & __goto_functions )

inlineexplicit

Definition at line 341 of file horn_encoding.cpp.

Member Function Documentation

◆ address_rec() [1/2]

exprt state_encodingt::address_rec	(	loct	loc,
		const exprt &	state,
		exprt	expr
	)		const

protected

Definition at line 412 of file state_encoding.cpp.

◆ address_rec() [2/2]

exprt state_encodingt::address_rec	(	loct	,
		const exprt &	,
		exprt
	)		const

protected

◆ assignment_constraint() [1/2]

exprt state_encodingt::assignment_constraint	(	loct	loc,
		exprt	lhs,
		exprt	rhs
	)		const

protected

Definition at line 588 of file state_encoding.cpp.

◆ assignment_constraint() [2/2]

exprt state_encodingt::assignment_constraint	(	loct	,
		exprt	lhs,
		exprt	rhs
	)		const

protected

◆ assignment_constraint_rec()

exprt state_encodingt::assignment_constraint_rec	(	loct	loc,
		exprt	state,
		exprt	lhs,
		exprt	rhs,
		std::vector< symbol_exprt > &	nondet_symbols
	)		const

protected

Definition at line 502 of file state_encoding.cpp.

◆ encode() [1/2]

void state_encodingt::encode	(	const goto_functiont &	goto_function,
		const irep_idt	function_identifier,
		const std::string &	state_prefix,
		const std::vector< irep_idt > &	call_stack,
		const std::string &	annotation,
		const symbol_exprt &	entry_state,
		const exprt &	return_lhs,
		encoding_targett &	dest
	)

Definition at line 929 of file state_encoding.cpp.

◆ encode() [2/2]

void state_encodingt::encode	(	const goto_functiont &	goto_function,
		const std::string &	state_prefix,
		const std::string &	annotation,
		const symbol_exprt &	entry_state,
		const exprt &	return_lhs,
		encoding_targett &	dest
	)

Definition at line 841 of file horn_encoding.cpp.

◆ evaluate_expr() [1/4]

exprt state_encodingt::evaluate_expr	(	loct	loc,
		const exprt &	what
	)		const

protected

Definition at line 381 of file state_encoding.cpp.

◆ evaluate_expr() [2/4]

exprt state_encodingt::evaluate_expr	(	loct	,
		const exprt &
	)		const

protected

◆ evaluate_expr() [3/4]

exprt state_encodingt::evaluate_expr	(	loct	loc,
		const exprt &	state,
		const exprt &	what
	)		const

protected

Definition at line 162 of file state_encoding.cpp.

◆ evaluate_expr() [4/4]

exprt state_encodingt::evaluate_expr	(	loct	,
		const exprt &	,
		const exprt &
	)		const

protected

◆ evaluate_expr_rec() [1/2]

exprt state_encodingt::evaluate_expr_rec	(	loct	loc,
		const exprt &	state,
		const exprt &	what,
		const std::unordered_set< symbol_exprt, irep_hash > &	bound_symbols
	)		const

protected

Definition at line 207 of file state_encoding.cpp.

◆ evaluate_expr_rec() [2/2]

exprt state_encodingt::evaluate_expr_rec	(	loct	,
		const exprt &	,
		const exprt &	,
		const std::unordered_set< symbol_exprt, irep_hash > &
	)		const

protected

◆ forall_states_expr() [1/4]

exprt state_encodingt::forall_states_expr	(	loct	loc,
		exprt	what
	)		const

protected

Definition at line 391 of file state_encoding.cpp.

◆ forall_states_expr() [2/4]

exprt state_encodingt::forall_states_expr	(	loct	,
		exprt
	)		const

protected

◆ forall_states_expr() [3/4]

exprt state_encodingt::forall_states_expr	(	loct	loc,
		exprt	condition,
		exprt	what
	)		const

protected

Definition at line 400 of file state_encoding.cpp.

◆ forall_states_expr() [4/4]

exprt state_encodingt::forall_states_expr	(	loct	,
		exprt	,
		exprt
	)		const

protected

◆ function_call() [1/2]

void state_encodingt::function_call	(	goto_programt::const_targett	loc,
		encoding_targett &	dest
	)

protected

Definition at line 875 of file state_encoding.cpp.

◆ function_call() [2/2]

void state_encodingt::function_call	(	goto_programt::const_targett	,
		encoding_targett &
	)

protected

◆ function_call_symbol() [1/2]

void state_encodingt::function_call_symbol	(	goto_programt::const_targett	loc,
		encoding_targett &	dest
	)

protected

Definition at line 647 of file state_encoding.cpp.

◆ function_call_symbol() [2/2]

void state_encodingt::function_call_symbol	(	goto_programt::const_targett	,
		encoding_targett &
	)

protected

◆ in_state_expr() [1/2]

symbol_exprt state_encodingt::in_state_expr ( loct loc ) const

protected

Definition at line 149 of file state_encoding.cpp.

◆ in_state_expr() [2/2]

symbol_exprt state_encodingt::in_state_expr ( loct ) const

protected

◆ incoming_symbols() [1/2]

std::vector< symbol_exprt > state_encodingt::incoming_symbols ( loct loc ) const

protected

Definition at line 122 of file state_encoding.cpp.

◆ incoming_symbols() [2/2]

std::vector< symbol_exprt > state_encodingt::incoming_symbols ( loct ) const

protected

◆ operator()() [1/2]

void state_encodingt::operator()	(	const goto_functionst::function_mapt::const_iterator	f_entry,
		encoding_targett &	dest
	)

Definition at line 898 of file state_encoding.cpp.

◆ operator()() [2/2]

void state_encodingt::operator()	(	const goto_functionst::function_mapt::const_iterator	,
		encoding_targett &
	)

◆ out_state_expr() [1/4]

symbol_exprt state_encodingt::out_state_expr ( loct loc ) const

protected

Definition at line 103 of file state_encoding.cpp.

◆ out_state_expr() [2/4]

symbol_exprt state_encodingt::out_state_expr ( loct ) const

protected

◆ out_state_expr() [3/4]

symbol_exprt state_encodingt::out_state_expr	(	loct	loc,
		bool	taken
	)		const

protected

Definition at line 117 of file state_encoding.cpp.

◆ out_state_expr() [4/4]

symbol_exprt state_encodingt::out_state_expr	(	loct	,
		bool	taken
	)		const

protected

◆ replace_nondet_rec() [1/2]

exprt state_encodingt::replace_nondet_rec	(	loct	loc,
		const exprt &	what,
		std::vector< symbol_exprt > &	nondet_symbols
	)		const

protected

Definition at line 170 of file state_encoding.cpp.

◆ replace_nondet_rec() [2/2]

exprt state_encodingt::replace_nondet_rec	(	loct	,
		const exprt &	,
		std::vector< symbol_exprt > &	nondet_symbols
	)		const

protected

◆ setup_incoming() [1/2]

void state_encodingt::setup_incoming ( const goto_functiont & goto_function )

protected

Definition at line 606 of file state_encoding.cpp.

◆ setup_incoming() [2/2]

void state_encodingt::setup_incoming ( const goto_functiont & )

protected

◆ state_expr_with_suffix() [1/2]

symbol_exprt state_encodingt::state_expr_with_suffix	(	loct	loc,
		const std::string &	suffix
	)		const

protected

Definition at line 108 of file state_encoding.cpp.

◆ state_expr_with_suffix() [2/2]

symbol_exprt state_encodingt::state_expr_with_suffix	(	loct	,
		const std::string &	suffix
	)		const

protected

◆ state_lambda_expr() [1/2]

exprt state_encodingt::state_lambda_expr ( exprt what )

staticprotected

Definition at line 386 of file state_encoding.cpp.

◆ state_lambda_expr() [2/2]

static exprt state_encodingt::state_lambda_expr ( exprt )

staticprotected

◆ va_args()

symbol_exprt state_encodingt::va_args ( irep_idt function )

staticprotected

Definition at line 638 of file state_encoding.cpp.

Member Data Documentation

◆ annotation

std::string state_encodingt::annotation

protected

Definition at line 91 of file state_encoding.cpp.

◆ call_stack

std::vector<irep_idt> state_encodingt::call_stack

protected

Definition at line 92 of file state_encoding.cpp.

◆ entry_state

symbol_exprt state_encodingt::entry_state = symbol_exprt(irep_idt(), typet())

protected

Definition at line 94 of file state_encoding.cpp.

◆ first_loc

loct state_encodingt::first_loc

protected

Definition at line 93 of file state_encoding.cpp.

◆ function_identifier

irep_idt state_encodingt::function_identifier

protected

Definition at line 89 of file state_encoding.cpp.

◆ goto_functions

const goto_functionst& state_encodingt::goto_functions

protected

Definition at line 360 of file horn_encoding.cpp.

◆ goto_model

const goto_modelt& state_encodingt::goto_model

protected

Definition at line 56 of file state_encoding.cpp.

◆ incoming

incomingt state_encodingt::incoming

protected

Definition at line 98 of file state_encoding.cpp.

◆ return_lhs

exprt state_encodingt::return_lhs = nil_exprt()

protected

Definition at line 95 of file state_encoding.cpp.

◆ state_prefix

std::string state_encodingt::state_prefix

protected

Definition at line 90 of file state_encoding.cpp.

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

/home/runner/work/cbmc/cbmc/src/cprover/state_encoding.cpp
/home/runner/work/cbmc/cbmc/src/goto-instrument/horn_encoding.cpp

Public Member Functions

Protected Types

Protected Member Functions

Static Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ incomingt [1/2]

◆ incomingt [2/2]

◆ loct [1/2]

◆ loct [2/2]

Constructor & Destructor Documentation

◆ state_encodingt() [1/2]

◆ state_encodingt() [2/2]

Member Function Documentation

◆ address_rec() [1/2]

◆ address_rec() [2/2]

◆ assignment_constraint() [1/2]

◆ assignment_constraint() [2/2]

◆ assignment_constraint_rec()

◆ encode() [1/2]

◆ encode() [2/2]

◆ evaluate_expr() [1/4]

◆ evaluate_expr() [2/4]

◆ evaluate_expr() [3/4]

◆ evaluate_expr() [4/4]

◆ evaluate_expr_rec() [1/2]

◆ evaluate_expr_rec() [2/2]

◆ forall_states_expr() [1/4]

◆ forall_states_expr() [2/4]

◆ forall_states_expr() [3/4]

◆ forall_states_expr() [4/4]

◆ function_call() [1/2]

◆ function_call() [2/2]

◆ function_call_symbol() [1/2]

◆ function_call_symbol() [2/2]

◆ in_state_expr() [1/2]

◆ in_state_expr() [2/2]

◆ incoming_symbols() [1/2]

◆ incoming_symbols() [2/2]

◆ operator()() [1/2]

◆ operator()() [2/2]

◆ out_state_expr() [1/4]

◆ out_state_expr() [2/4]

◆ out_state_expr() [3/4]

◆ out_state_expr() [4/4]

◆ replace_nondet_rec() [1/2]

◆ replace_nondet_rec() [2/2]

◆ setup_incoming() [1/2]

◆ setup_incoming() [2/2]

◆ state_expr_with_suffix() [1/2]

◆ state_expr_with_suffix() [2/2]

◆ state_lambda_expr() [1/2]

◆ state_lambda_expr() [2/2]

◆ va_args()

Member Data Documentation

◆ annotation

◆ call_stack

◆ entry_state

◆ first_loc

◆ function_identifier

◆ goto_functions

◆ goto_model

◆ incoming

◆ return_lhs

◆ state_prefix