CBMC
|
This is the complete list of members for state_encodingt, including all inherited members.
address_rec(loct, const exprt &, exprt) const | state_encodingt | protected |
address_rec(loct, const exprt &, exprt) const | state_encodingt | protected |
annotation | state_encodingt | protected |
assignment_constraint(loct, exprt lhs, exprt rhs) const | state_encodingt | protected |
assignment_constraint(loct, exprt lhs, exprt rhs) const | state_encodingt | protected |
assignment_constraint_rec(loct, exprt state, exprt lhs, exprt rhs, std::vector< symbol_exprt > &nondet_symbols) const | state_encodingt | protected |
call_stack | state_encodingt | protected |
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_state | state_encodingt | protected |
evaluate_expr(loct, const exprt &, const exprt &) const | state_encodingt | protected |
evaluate_expr(loct, const exprt &) const | state_encodingt | protected |
evaluate_expr(loct, const exprt &, const exprt &) const | state_encodingt | protected |
evaluate_expr(loct, const exprt &) const | state_encodingt | protected |
evaluate_expr_rec(loct, const exprt &, const exprt &, const std::unordered_set< symbol_exprt, irep_hash > &) const | state_encodingt | protected |
evaluate_expr_rec(loct, const exprt &, const exprt &, const std::unordered_set< symbol_exprt, irep_hash > &) const | state_encodingt | protected |
first_loc | state_encodingt | protected |
forall_states_expr(loct, exprt) const | state_encodingt | protected |
forall_states_expr(loct, exprt, exprt) const | state_encodingt | protected |
forall_states_expr(loct, exprt) const | state_encodingt | protected |
forall_states_expr(loct, exprt, exprt) const | state_encodingt | protected |
function_call(goto_programt::const_targett, encoding_targett &) | state_encodingt | protected |
function_call(goto_programt::const_targett, encoding_targett &) | state_encodingt | protected |
function_call_symbol(goto_programt::const_targett, encoding_targett &) | state_encodingt | protected |
function_call_symbol(goto_programt::const_targett, encoding_targett &) | state_encodingt | protected |
function_identifier | state_encodingt | protected |
goto_functions | state_encodingt | protected |
goto_model | state_encodingt | protected |
in_state_expr(loct) const | state_encodingt | protected |
in_state_expr(loct) const | state_encodingt | protected |
incoming | state_encodingt | protected |
incoming_symbols(loct) const | state_encodingt | protected |
incoming_symbols(loct) const | state_encodingt | protected |
incomingt typedef | state_encodingt | protected |
incomingt typedef | state_encodingt | protected |
loct typedef | state_encodingt | protected |
loct typedef | state_encodingt | protected |
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) const | state_encodingt | protected |
out_state_expr(loct, bool taken) const | state_encodingt | protected |
out_state_expr(loct) const | state_encodingt | protected |
out_state_expr(loct, bool taken) const | state_encodingt | protected |
replace_nondet_rec(loct, const exprt &, std::vector< symbol_exprt > &nondet_symbols) const | state_encodingt | protected |
replace_nondet_rec(loct, const exprt &, std::vector< symbol_exprt > &nondet_symbols) const | state_encodingt | protected |
return_lhs | state_encodingt | protected |
setup_incoming(const goto_functiont &) | state_encodingt | protected |
setup_incoming(const goto_functiont &) | state_encodingt | protected |
state_encodingt(const goto_modelt &__goto_model) | state_encodingt | inlineexplicit |
state_encodingt(const goto_functionst &__goto_functions) | state_encodingt | inlineexplicit |
state_expr_with_suffix(loct, const std::string &suffix) const | state_encodingt | protected |
state_expr_with_suffix(loct, const std::string &suffix) const | state_encodingt | protected |
state_lambda_expr(exprt) | state_encodingt | protectedstatic |
state_lambda_expr(exprt) | state_encodingt | protectedstatic |
state_prefix | state_encodingt | protected |
va_args(irep_idt function) | state_encodingt | protectedstatic |