Collaboration diagram for state_encodingt:

Public Member Functions
	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 > >

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

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)

Protected Attributes
const goto_functionst &	goto_functions

std::string	state_prefix

std::string	annotation

loct	first_loc

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

exprt	return_lhs = nil_exprt()

incomingt	incoming

Detailed Description

Definition at line 338 of file horn_encoding.cpp.

Member Typedef Documentation

◆ incomingt

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

protected

Definition at line 392 of file horn_encoding.cpp.

◆ loct

using state_encodingt::loct = goto_programt::const_targett

protected

Definition at line 359 of file horn_encoding.cpp.

Constructor & Destructor Documentation

◆ state_encodingt()

state_encodingt::state_encodingt ( const goto_functionst & __goto_functions )

inlineexplicit

Definition at line 341 of file horn_encoding.cpp.

Member Function Documentation

◆ address_rec()

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

protected

Definition at line 585 of file horn_encoding.cpp.

◆ assignment_constraint()

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

protected

Definition at line 652 of file horn_encoding.cpp.

◆ encode()

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 840 of file horn_encoding.cpp.

◆ evaluate_expr() [1/2]

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

protected

Definition at line 554 of file horn_encoding.cpp.

◆ evaluate_expr() [2/2]

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

protected

Definition at line 455 of file horn_encoding.cpp.

◆ evaluate_expr_rec()

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 492 of file horn_encoding.cpp.

◆ forall_states_expr() [1/2]

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

protected

Definition at line 564 of file horn_encoding.cpp.

◆ forall_states_expr() [2/2]

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

protected

Definition at line 573 of file horn_encoding.cpp.

◆ function_call()

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

protected

Definition at line 795 of file horn_encoding.cpp.

◆ function_call_symbol()

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

protected

Definition at line 708 of file horn_encoding.cpp.

◆ in_state_expr()

symbol_exprt state_encodingt::in_state_expr ( loct loc ) const

protected

Definition at line 442 of file horn_encoding.cpp.

◆ incoming_symbols()

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

protected

Definition at line 415 of file horn_encoding.cpp.

◆ operator()()

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

Definition at line 818 of file horn_encoding.cpp.

◆ out_state_expr() [1/2]

symbol_exprt state_encodingt::out_state_expr ( loct loc ) const

protected

Definition at line 396 of file horn_encoding.cpp.

◆ out_state_expr() [2/2]

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

protected

Definition at line 410 of file horn_encoding.cpp.

◆ replace_nondet_rec()

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

protected

Definition at line 463 of file horn_encoding.cpp.

◆ setup_incoming()

void state_encodingt::setup_incoming ( const goto_functiont & goto_function )

protected

Definition at line 676 of file horn_encoding.cpp.

◆ state_expr_with_suffix()

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

protected

Definition at line 401 of file horn_encoding.cpp.

◆ state_lambda_expr()

exprt state_encodingt::state_lambda_expr ( exprt what )

staticprotected

Definition at line 559 of file horn_encoding.cpp.

Member Data Documentation

◆ annotation

std::string state_encodingt::annotation

protected

Definition at line 388 of file horn_encoding.cpp.

◆ entry_state

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

protected

Definition at line 390 of file horn_encoding.cpp.

◆ first_loc

loct state_encodingt::first_loc

protected

Definition at line 389 of file horn_encoding.cpp.

◆ goto_functions

const goto_functionst& state_encodingt::goto_functions

protected

Definition at line 360 of file horn_encoding.cpp.

◆ incoming

incomingt state_encodingt::incoming

protected

Definition at line 393 of file horn_encoding.cpp.

◆ return_lhs

exprt state_encodingt::return_lhs = nil_exprt()

protected

Definition at line 391 of file horn_encoding.cpp.

◆ state_prefix

std::string state_encodingt::state_prefix

protected

Definition at line 387 of file horn_encoding.cpp.

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

/home/runner/work/cbmc-documentation/cbmc-documentation/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

◆ loct

Constructor & Destructor Documentation

◆ state_encodingt()

Member Function Documentation

◆ address_rec()

◆ assignment_constraint()

◆ encode()

◆ evaluate_expr() [1/2]

◆ evaluate_expr() [2/2]

◆ evaluate_expr_rec()

◆ forall_states_expr() [1/2]

◆ forall_states_expr() [2/2]

◆ function_call()

◆ function_call_symbol()

◆ in_state_expr()

◆ incoming_symbols()

◆ operator()()

◆ out_state_expr() [1/2]

◆ out_state_expr() [2/2]

◆ replace_nondet_rec()

◆ setup_incoming()

◆ state_expr_with_suffix()

◆ state_lambda_expr()

Member Data Documentation

◆ annotation

◆ entry_state

◆ first_loc

◆ goto_functions

◆ incoming

◆ return_lhs

◆ state_prefix