cprover
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_symextprotected
add_to_lhs(const exprt &lhs, const exprt &what)goto_symextprotectedstatic
address_arithmetic(const exprt &expr, statet &state, guardt &guard, bool keep_array)goto_symextprotected
assignment_typet typedefgoto_symextprotected
atomic_section_countergoto_symextprotected
body_warningssymex_bmctprotected
clean_expr(exprt &expr, statet &state, bool write)goto_symextprotected
constant_propagationgoto_symext
debug()messagetinline
dereference(exprt &expr, statet &state, const bool write)goto_symextprotectedvirtual
dereference_rec(exprt &expr, statet &state, guardt &guard, const bool write)goto_symextprotected
dereference_rec_address_of(exprt &expr, statet &state, guardt &guard)goto_symextprotected
do_simplify(exprt &expr)goto_symextprotectedvirtual
dynamic_countergoto_symextprotectedstatic
endl(mstreamt &m)messagetinlinestatic
eom(mstreamt &m)messagetinlinestatic
error()messagetinline
get_message_handler()messagetinline
get_mstream(unsigned message_level)messagetinline
get_unwind(const symex_targett::sourcet &source, unsigned unwind)symex_bmctprotectedvirtual
get_unwind_recursion(const irep_idt &identifier, const unsigned thread_nr, unsigned unwind)symex_bmctprotectedvirtual
goto_symext(const namespacet &_ns, symbol_tablet &_new_symbol_table, symex_targett &_target)goto_symextinline
guard_identifiergoto_symextprotected
initialize_auto_object(const exprt &expr, statet &state)goto_symextprotected
is_index_member_symbol_if(const exprt &expr)goto_symextprotectedstatic
language_modegoto_symext
last_source_locationsymex_bmct
locality(const irep_idt function_identifier, statet &state, const goto_functionst::goto_functiont &goto_function)goto_symextprotected
loop_bound_exceeded(statet &state, const exprt &guard)goto_symextprotectedvirtual
loop_limitssymex_bmctprotected
loop_limitst typedefsymex_bmctprotected
M_DEBUG enum valuemessaget
M_ERROR enum valuemessaget
M_PROGRESS enum valuemessaget
M_RESULT enum valuemessaget
M_STATISTICS enum valuemessaget
M_STATUS enum valuemessaget
M_WARNING enum valuemessaget
make_auto_object(const typet &type)goto_symextprotected
max_unwindsymex_bmctprotected
max_unwind_is_setsymex_bmctprotected
merge_goto(const statet::goto_statet &goto_state, statet &state)symex_bmctprotectedvirtual
merge_gotos(statet &state)goto_symextprotected
merge_value_sets(const statet::goto_statet &goto_state, statet &dest)goto_symextprotected
message_handlermessagetprotected
message_levelt enum namemessaget
messaget()messagetinline
messaget(const messaget &other)messagetinline
messaget(message_handlert &_message_handler)messagetinlineexplicit
mstreammessagetprotected
new_name(symbolt &symbol)goto_symextprotected
new_symbol_tablegoto_symext
no_body(const irep_idt &identifier)symex_bmctprotectedvirtual
nondet_countgoto_symextprotectedstatic
nsgoto_symextprotected
operator()(const goto_functionst &goto_functions)goto_symextvirtual
operator()(const goto_functionst &goto_functions, const goto_programt &goto_program)goto_symextvirtual
operator()(statet &state, const goto_functionst &goto_functions, const goto_programt &goto_program)goto_symextvirtual
optionsgoto_symext
output_coverage_report(const goto_functionst &goto_functions, const std::string &path) constsymex_bmctinline
parameter_assignments(const irep_idt function_identifier, const goto_functionst::goto_functiont &goto_function, statet &state, const exprt::operandst &arguments)goto_symextprotected
phi_function(const statet::goto_statet &goto_state, statet &state)goto_symextprotected
pop_frame(statet &state)goto_symextprotected
process_array_expr(exprt &expr)goto_symextprotected
process_array_expr_rec(exprt &expr, const typet &type) constgoto_symextprotected
progress()messagetinline
read(exprt &expr)goto_symextprotected
record_coveragesymex_bmct
remaining_vccsgoto_symext
replace_array_equal(exprt &expr)goto_symextprotected
replace_nondet(exprt &expr)goto_symextprotected
result()messagetinline
return_assignment(statet &state)goto_symextprotected
rewrite_quantifiers(exprt &expr, statet &state)goto_symextprotected
set_message_handler(message_handlert &_message_handler)messagetinlinevirtual
set_unwind_limit(unsigned limit)symex_bmctinline
set_unwind_loop_limit(const irep_idt &id, unsigned limit)symex_bmctinline
set_unwind_thread_loop_limit(unsigned thread_nr, const irep_idt &id, unsigned limit)symex_bmctinline
statet typedefgoto_symext
statistics()messagetinline
status()messagetinline
symex_assign(statet &state, const code_assignt &code)goto_symextprotectedvirtual
symex_assign_array(statet &state, const index_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)goto_symextprotected
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_symextprotected
symex_assign_if(statet &state, const if_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)goto_symextprotected
symex_assign_rec(statet &state, const code_assignt &code)goto_symextprotected
symex_assign_rec(statet &state, const exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)goto_symextprotected
symex_assign_struct_member(statet &state, const member_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)goto_symextprotected
symex_assign_symbol(statet &state, const ssa_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)goto_symextprotected
symex_assign_typecast(statet &state, const typecast_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)goto_symextprotected
symex_assume(statet &state, const exprt &cond)goto_symextprotectedvirtual
symex_atomic_begin(statet &state)goto_symextprotectedvirtual
symex_atomic_end(statet &state)goto_symextprotectedvirtual
symex_bmct(const namespacet &_ns, symbol_tablet &_new_symbol_table, symex_targett &_target)symex_bmct
symex_catch(statet &state)goto_symextprotected
symex_coveragesymex_bmctprotected
symex_cpp_delete(statet &state, const codet &code)goto_symextprotectedvirtual
symex_cpp_new(statet &state, const exprt &lhs, const side_effect_exprt &code)goto_symextprotectedvirtual
symex_dead(statet &state)goto_symextprotectedvirtual
symex_decl(statet &state)goto_symextprotectedvirtual
symex_decl(statet &state, const symbol_exprt &expr)goto_symextprotectedvirtual
symex_end_of_function(statet &state)goto_symextprotectedvirtual
symex_fkt(statet &state, const code_function_callt &code)goto_symextprotectedvirtual
symex_function_call(const goto_functionst &goto_functions, statet &state, const code_function_callt &call)goto_symextprotectedvirtual
symex_function_call_code(const goto_functionst &goto_functions, statet &state, const code_function_callt &call)goto_symextprotectedvirtual
symex_function_call_symbol(const goto_functionst &goto_functions, statet &state, const code_function_callt &call)goto_symextprotectedvirtual
symex_gcc_builtin_va_arg_next(statet &state, const exprt &lhs, const side_effect_exprt &code)goto_symextprotectedvirtual
symex_goto(statet &state)goto_symextprotectedvirtual
symex_input(statet &state, const codet &code)goto_symextprotectedvirtual
symex_macro(statet &state, const code_function_callt &code)goto_symextprotectedvirtual
symex_malloc(statet &state, const exprt &lhs, const side_effect_exprt &code)goto_symextprotectedvirtual
symex_other(const goto_functionst &goto_functions, statet &state)goto_symextprotectedvirtual
symex_output(statet &state, const codet &code)goto_symextprotectedvirtual
symex_printf(statet &state, const exprt &lhs, const exprt &rhs)goto_symextprotectedvirtual
symex_start_thread(statet &state)goto_symextprotectedvirtual
symex_step(const goto_functionst &goto_functions, statet &state)symex_bmctprotectedvirtual
symex_step_goto(statet &state, bool taken)goto_symextvirtual
symex_throw(statet &state)goto_symextprotected
symex_trace(statet &state, const code_function_callt &code)goto_symextprotectedvirtual
symex_transition(statet &state, goto_programt::const_targett to, bool is_backwards_goto=false)goto_symextprotectedvirtual
symex_transition(statet &state)goto_symextinlineprotectedvirtual
targetgoto_symextprotected
thread_loop_limitssymex_bmctprotected
thread_loop_limitst typedefsymex_bmctprotected
total_vccsgoto_symext
trigger_auto_object(const exprt &expr, statet &state)goto_symextprotected
vcc(const exprt &expr, const std::string &msg, statet &state)goto_symextprotectedvirtual
warning()messagetinline
~goto_symext()goto_symextinlinevirtual
~messaget()messagetvirtual