symex_bmct Member List

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

add_end_of_function(exprt &code, const irep_idt &identifier)	goto_symext	protected
add_to_lhs(const exprt &lhs, const exprt &what)	goto_symext	protectedstatic
address_arithmetic(const exprt &expr, statet &state, guardt &guard, bool keep_array)	goto_symext	protected
assignment_typet typedef	goto_symext	protected
atomic_section_counter	goto_symext	protected
body_warnings	symex_bmct	protected
clean_expr(exprt &expr, statet &state, bool write)	goto_symext	protected
constant_propagation	goto_symext
debug()	messaget	inline
dereference(exprt &expr, statet &state, const bool write)	goto_symext	protectedvirtual
dereference_rec(exprt &expr, statet &state, guardt &guard, const bool write)	goto_symext	protected
dereference_rec_address_of(exprt &expr, statet &state, guardt &guard)	goto_symext	protected
do_simplify(exprt &expr)	goto_symext	protectedvirtual
dynamic_counter	goto_symext	protectedstatic
endl(mstreamt &m)	messaget	inlinestatic
eom(mstreamt &m)	messaget	inlinestatic
error()	messaget	inline
get_message_handler()	messaget	inline
get_mstream(unsigned message_level)	messaget	inline
get_unwind(const symex_targett::sourcet &source, unsigned unwind)	symex_bmct	protectedvirtual
get_unwind_recursion(const irep_idt &identifier, const unsigned thread_nr, unsigned unwind)	symex_bmct	protectedvirtual
goto_symext(const namespacet &_ns, symbol_tablet &_new_symbol_table, symex_targett &_target)	goto_symext	inline
guard_identifier	goto_symext	protected
initialize_auto_object(const exprt &expr, statet &state)	goto_symext	protected
is_index_member_symbol_if(const exprt &expr)	goto_symext	protectedstatic
language_mode	goto_symext
last_source_location	symex_bmct
locality(const irep_idt function_identifier, statet &state, const goto_functionst::goto_functiont &goto_function)	goto_symext	protected
loop_bound_exceeded(statet &state, const exprt &guard)	goto_symext	protectedvirtual
loop_limits	symex_bmct	protected
loop_limitst typedef	symex_bmct	protected
M_DEBUG enum value	messaget
M_ERROR enum value	messaget
M_PROGRESS enum value	messaget
M_RESULT enum value	messaget
M_STATISTICS enum value	messaget
M_STATUS enum value	messaget
M_WARNING enum value	messaget
make_auto_object(const typet &type)	goto_symext	protected
max_unwind	symex_bmct	protected
max_unwind_is_set	symex_bmct	protected
merge_goto(const statet::goto_statet &goto_state, statet &state)	symex_bmct	protectedvirtual
merge_gotos(statet &state)	goto_symext	protected
merge_value_sets(const statet::goto_statet &goto_state, statet &dest)	goto_symext	protected
message_handler	messaget	protected
message_levelt enum name	messaget
messaget()	messaget	inline
messaget(const messaget &other)	messaget	inline
messaget(message_handlert &_message_handler)	messaget	inlineexplicit
mstream	messaget	protected
new_name(symbolt &symbol)	goto_symext	protected
new_symbol_table	goto_symext
no_body(const irep_idt &identifier)	symex_bmct	protectedvirtual
nondet_count	goto_symext	protectedstatic
ns	goto_symext	protected
operator()(const goto_functionst &goto_functions)	goto_symext	virtual
operator()(const goto_functionst &goto_functions, const goto_programt &goto_program)	goto_symext	virtual
operator()(statet &state, const goto_functionst &goto_functions, const goto_programt &goto_program)	goto_symext	virtual
options	goto_symext
output_coverage_report(const goto_functionst &goto_functions, const std::string &path) const	symex_bmct	inline
parameter_assignments(const irep_idt function_identifier, const goto_functionst::goto_functiont &goto_function, statet &state, const exprt::operandst &arguments)	goto_symext	protected
phi_function(const statet::goto_statet &goto_state, statet &state)	goto_symext	protected
pop_frame(statet &state)	goto_symext	protected
process_array_expr(exprt &expr)	goto_symext	protected
process_array_expr_rec(exprt &expr, const typet &type) const	goto_symext	protected
progress()	messaget	inline
read(exprt &expr)	goto_symext	protected
record_coverage	symex_bmct
remaining_vccs	goto_symext
replace_array_equal(exprt &expr)	goto_symext	protected
replace_nondet(exprt &expr)	goto_symext	protected
result()	messaget	inline
return_assignment(statet &state)	goto_symext	protected
rewrite_quantifiers(exprt &expr, statet &state)	goto_symext	protected
set_message_handler(message_handlert &_message_handler)	messaget	inlinevirtual
set_unwind_limit(unsigned limit)	symex_bmct	inline
set_unwind_loop_limit(const irep_idt &id, unsigned limit)	symex_bmct	inline
set_unwind_thread_loop_limit(unsigned thread_nr, const irep_idt &id, unsigned limit)	symex_bmct	inline
statet typedef	goto_symext
statistics()	messaget	inline
status()	messaget	inline
symex_assign(statet &state, const code_assignt &code)	goto_symext	protectedvirtual
symex_assign_array(statet &state, const index_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)	goto_symext	protected
symex_assign_byte_extract(statet &state, const byte_extract_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)	goto_symext	protected
symex_assign_if(statet &state, const if_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)	goto_symext	protected
symex_assign_rec(statet &state, const code_assignt &code)	goto_symext	protected
symex_assign_rec(statet &state, const exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)	goto_symext	protected
symex_assign_struct_member(statet &state, const member_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)	goto_symext	protected
symex_assign_symbol(statet &state, const ssa_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)	goto_symext	protected
symex_assign_typecast(statet &state, const typecast_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)	goto_symext	protected
symex_assume(statet &state, const exprt &cond)	goto_symext	protectedvirtual
symex_atomic_begin(statet &state)	goto_symext	protectedvirtual
symex_atomic_end(statet &state)	goto_symext	protectedvirtual
symex_bmct(const namespacet &_ns, symbol_tablet &_new_symbol_table, symex_targett &_target)	symex_bmct
symex_catch(statet &state)	goto_symext	protected
symex_coverage	symex_bmct	protected
symex_cpp_delete(statet &state, const codet &code)	goto_symext	protectedvirtual
symex_cpp_new(statet &state, const exprt &lhs, const side_effect_exprt &code)	goto_symext	protectedvirtual
symex_dead(statet &state)	goto_symext	protectedvirtual
symex_decl(statet &state)	goto_symext	protectedvirtual
symex_decl(statet &state, const symbol_exprt &expr)	goto_symext	protectedvirtual
symex_end_of_function(statet &state)	goto_symext	protectedvirtual
symex_fkt(statet &state, const code_function_callt &code)	goto_symext	protectedvirtual
symex_function_call(const goto_functionst &goto_functions, statet &state, const code_function_callt &call)	goto_symext	protectedvirtual
symex_function_call_code(const goto_functionst &goto_functions, statet &state, const code_function_callt &call)	goto_symext	protectedvirtual
symex_function_call_symbol(const goto_functionst &goto_functions, statet &state, const code_function_callt &call)	goto_symext	protectedvirtual
symex_gcc_builtin_va_arg_next(statet &state, const exprt &lhs, const side_effect_exprt &code)	goto_symext	protectedvirtual
symex_goto(statet &state)	goto_symext	protectedvirtual
symex_input(statet &state, const codet &code)	goto_symext	protectedvirtual
symex_macro(statet &state, const code_function_callt &code)	goto_symext	protectedvirtual
symex_malloc(statet &state, const exprt &lhs, const side_effect_exprt &code)	goto_symext	protectedvirtual
symex_other(const goto_functionst &goto_functions, statet &state)	goto_symext	protectedvirtual
symex_output(statet &state, const codet &code)	goto_symext	protectedvirtual
symex_printf(statet &state, const exprt &lhs, const exprt &rhs)	goto_symext	protectedvirtual
symex_start_thread(statet &state)	goto_symext	protectedvirtual
symex_step(const goto_functionst &goto_functions, statet &state)	symex_bmct	protectedvirtual
symex_step_goto(statet &state, bool taken)	goto_symext	virtual
symex_throw(statet &state)	goto_symext	protected
symex_trace(statet &state, const code_function_callt &code)	goto_symext	protectedvirtual
symex_transition(statet &state, goto_programt::const_targett to, bool is_backwards_goto=false)	goto_symext	protectedvirtual
symex_transition(statet &state)	goto_symext	inlineprotectedvirtual
target	goto_symext	protected
thread_loop_limits	symex_bmct	protected
thread_loop_limitst typedef	symex_bmct	protected
total_vccs	goto_symext
trigger_auto_object(const exprt &expr, statet &state)	goto_symext	protected
vcc(const exprt &expr, const std::string &msg, statet &state)	goto_symext	protectedvirtual
warning()	messaget	inline
~goto_symext()	goto_symext	inlinevirtual
~messaget()	messaget	virtual