state_encodingt Class Reference

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
using	loct = goto_programt::const_targett
using	incomingt

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

protected

Initial value:

Definition at line 96 of file state_encoding.cpp.

incomingt [2/2]

using state_encodingt::incomingt

protected

Initial value:

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:

• cprover/state_encoding.cpp
• goto-instrument/horn_encoding.cpp