CBMC
state_encodingt Member List

This is the complete list of members for state_encodingt, including all inherited members.

address_rec(loct, const exprt &, exprt) conststate_encodingtprotected
address_rec(loct, const exprt &, exprt) conststate_encodingtprotected
annotationstate_encodingtprotected
assignment_constraint(loct, exprt lhs, exprt rhs) conststate_encodingtprotected
assignment_constraint(loct, exprt lhs, exprt rhs) conststate_encodingtprotected
assignment_constraint_rec(loct, exprt state, exprt lhs, exprt rhs, std::vector< symbol_exprt > &nondet_symbols) conststate_encodingtprotected
call_stackstate_encodingtprotected
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
encode(const goto_functiont &, const std::string &state_prefix, const std::string &annotation, const symbol_exprt &entry_state, const exprt &return_lhs, encoding_targett &)state_encodingt
entry_statestate_encodingtprotected
evaluate_expr(loct, const exprt &, const exprt &) conststate_encodingtprotected
evaluate_expr(loct, const exprt &) conststate_encodingtprotected
evaluate_expr(loct, const exprt &, const exprt &) conststate_encodingtprotected
evaluate_expr(loct, const exprt &) conststate_encodingtprotected
evaluate_expr_rec(loct, const exprt &, const exprt &, const std::unordered_set< symbol_exprt, irep_hash > &) conststate_encodingtprotected
evaluate_expr_rec(loct, const exprt &, const exprt &, const std::unordered_set< symbol_exprt, irep_hash > &) conststate_encodingtprotected
first_locstate_encodingtprotected
forall_states_expr(loct, exprt) conststate_encodingtprotected
forall_states_expr(loct, exprt, exprt) conststate_encodingtprotected
forall_states_expr(loct, exprt) conststate_encodingtprotected
forall_states_expr(loct, exprt, exprt) conststate_encodingtprotected
function_call(goto_programt::const_targett, encoding_targett &)state_encodingtprotected
function_call(goto_programt::const_targett, encoding_targett &)state_encodingtprotected
function_call_symbol(goto_programt::const_targett, encoding_targett &)state_encodingtprotected
function_call_symbol(goto_programt::const_targett, encoding_targett &)state_encodingtprotected
function_identifierstate_encodingtprotected
goto_functionsstate_encodingtprotected
goto_modelstate_encodingtprotected
in_state_expr(loct) conststate_encodingtprotected
in_state_expr(loct) conststate_encodingtprotected
incomingstate_encodingtprotected
incoming_symbols(loct) conststate_encodingtprotected
incoming_symbols(loct) conststate_encodingtprotected
incomingt typedefstate_encodingtprotected
incomingt typedefstate_encodingtprotected
loct typedefstate_encodingtprotected
loct typedefstate_encodingtprotected
operator()(const goto_functionst::function_mapt::const_iterator, encoding_targett &)state_encodingt
operator()(const goto_functionst::function_mapt::const_iterator, encoding_targett &)state_encodingt
out_state_expr(loct) conststate_encodingtprotected
out_state_expr(loct, bool taken) conststate_encodingtprotected
out_state_expr(loct) conststate_encodingtprotected
out_state_expr(loct, bool taken) conststate_encodingtprotected
replace_nondet_rec(loct, const exprt &, std::vector< symbol_exprt > &nondet_symbols) conststate_encodingtprotected
replace_nondet_rec(loct, const exprt &, std::vector< symbol_exprt > &nondet_symbols) conststate_encodingtprotected
return_lhsstate_encodingtprotected
setup_incoming(const goto_functiont &)state_encodingtprotected
setup_incoming(const goto_functiont &)state_encodingtprotected
state_encodingt(const goto_modelt &__goto_model)state_encodingtinlineexplicit
state_encodingt(const goto_functionst &__goto_functions)state_encodingtinlineexplicit
state_expr_with_suffix(loct, const std::string &suffix) conststate_encodingtprotected
state_expr_with_suffix(loct, const std::string &suffix) conststate_encodingtprotected
state_lambda_expr(exprt)state_encodingtprotectedstatic
state_lambda_expr(exprt)state_encodingtprotectedstatic
state_prefixstate_encodingtprotected
va_args(irep_idt function)state_encodingtprotectedstatic