cprover
goto_symext Member List

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

_remaining_vccsgoto_symextprotected
_total_vccsgoto_symextprotected
add_to_lhs(const exprt &lhs, const exprt &what)goto_symextprotectedstatic
address_arithmetic(const exprt &, statet &, guardt &, bool keep_array)goto_symextprotected
assignment_typet typedefgoto_symextprotected
atomic_section_countergoto_symextprotected
build_symex_nondetgoto_symextprotected
clean_expr(exprt &, statet &, bool write)goto_symextprotected
dereference(exprt &, statet &, bool write)goto_symextprotectedvirtual
dereference_rec(exprt &, statet &, guardt &, bool write)goto_symextprotected
dereference_rec_address_of(exprt &, statet &, guardt &)goto_symextprotected
do_simplify(exprt &)goto_symextprotectedvirtual
dynamic_countergoto_symextprotectedstatic
get_goto_functiont typedefgoto_symext
get_remaining_vccs()goto_symextinline
get_total_vccs()goto_symextinline
get_unwind_recursion(const irep_idt &identifier, unsigned thread_nr, unsigned unwind)goto_symextprotectedvirtual
goto_symext(message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage)goto_symextinline
guard_identifiergoto_symextprotected
havoc_rec(statet &, const guardt &, const exprt &)goto_symextprotected
initialize_auto_object(const exprt &, statet &)goto_symextprotected
initialize_entry_point(statet &state, const get_goto_functiont &get_goto_function, const irep_idt &function_identifier, goto_programt::const_targett pc, goto_programt::const_targett limit)goto_symextprotected
is_index_member_symbol_if(const exprt &expr)goto_symextprotectedstatic
language_modegoto_symext
locality(const irep_idt &function_identifier, statet &, const goto_functionst::goto_functiont &)goto_symextprotected
loggoto_symextmutableprotected
loop_bound_exceeded(statet &, const exprt &guard)goto_symextprotectedvirtual
make_auto_object(const typet &, statet &)goto_symextprotected
merge_goto(const statet::goto_statet &goto_state, statet &)goto_symextprotectedvirtual
merge_gotos(statet &)goto_symextprotected
merge_value_sets(const statet::goto_statet &goto_state, statet &dest)goto_symextprotected
no_body(const irep_idt &)goto_symextinlineprotectedvirtual
nsgoto_symextprotected
outer_symbol_tablegoto_symextprotected
parameter_assignments(const irep_idt &function_identifier, const goto_functionst::goto_functiont &, statet &, const exprt::operandst &arguments)goto_symextprotected
path_segment_vccsgoto_symext
path_storagegoto_symextprotected
phi_function(const statet::goto_statet &goto_state, statet &)goto_symextprotected
pop_frame(statet &)goto_symextprotected
process_array_expr(exprt &)goto_symextprotected
resume_symex_from_saved_state(const get_goto_functiont &get_goto_function, const statet &saved_state, symex_target_equationt *saved_equation, symbol_tablet &new_symbol_table)goto_symextvirtual
return_assignment(statet &)goto_symextprotected
rewrite_quantifiers(exprt &, statet &)goto_symextprotected
should_pause_symexgoto_symext
should_stop_unwind(const symex_targett::sourcet &source, const goto_symex_statet::call_stackt &context, unsigned unwind)goto_symextprotectedvirtual
statet typedefgoto_symext
symex_allocate(statet &, const exprt &lhs, const side_effect_exprt &)goto_symextprotectedvirtual
symex_assign(statet &, const code_assignt &)goto_symextprotected
symex_assign_array(statet &, const index_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)goto_symextprotected
symex_assign_byte_extract(statet &, const byte_extract_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)goto_symextprotected
symex_assign_if(statet &, const if_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)goto_symextprotected
symex_assign_rec(statet &, const exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)goto_symextprotected
symex_assign_struct_member(statet &, const member_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)goto_symextprotected
symex_assign_symbol(statet &, const ssa_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)goto_symextprotected
symex_assign_typecast(statet &, const typecast_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)goto_symextprotected
symex_assume(statet &, const exprt &cond)goto_symextprotectedvirtual
symex_atomic_begin(statet &)goto_symextprotectedvirtual
symex_atomic_end(statet &)goto_symextprotectedvirtual
symex_catch(statet &)goto_symextprotected
symex_configgoto_symextprotected
symex_cpp_delete(statet &, const codet &)goto_symextprotectedvirtual
symex_cpp_new(statet &, const exprt &lhs, const side_effect_exprt &)goto_symextprotectedvirtual
symex_dead(statet &)goto_symextprotectedvirtual
symex_decl(statet &)goto_symextprotectedvirtual
symex_decl(statet &, const symbol_exprt &expr)goto_symextprotectedvirtual
symex_dereference_statet classgoto_symextfriend
symex_end_of_function(statet &)goto_symextprotectedvirtual
symex_fkt(statet &, const code_function_callt &)goto_symextprotectedvirtual
symex_from_entry_point_of(const get_goto_functiont &get_goto_function, symbol_tablet &new_symbol_table)goto_symextvirtual
symex_function_call(const get_goto_functiont &, statet &, const code_function_callt &)goto_symextprotectedvirtual
symex_function_call_code(const get_goto_functiont &, statet &, const code_function_callt &)goto_symextprotectedvirtual
symex_function_call_symbol(const get_goto_functiont &, statet &, const code_function_callt &)goto_symextprotectedvirtual
symex_gcc_builtin_va_arg_next(statet &, const exprt &lhs, const side_effect_exprt &)goto_symextprotectedvirtual
symex_goto(statet &)goto_symextprotectedvirtual
symex_input(statet &, const codet &)goto_symextprotectedvirtual
symex_macro(statet &, const code_function_callt &)goto_symextprotectedvirtual
symex_other(statet &)goto_symextprotectedvirtual
symex_output(statet &, const codet &)goto_symextprotectedvirtual
symex_printf(statet &, const exprt &rhs)goto_symextprotectedvirtual
symex_start_thread(statet &)goto_symextprotectedvirtual
symex_step(const get_goto_functiont &, statet &)goto_symextprotectedvirtual
symex_threaded_step(statet &, const get_goto_functiont &)goto_symextprotected
symex_throw(statet &)goto_symextprotected
symex_trace(statet &, const code_function_callt &)goto_symextprotectedvirtual
symex_with_state(statet &, const goto_functionst &, symbol_tablet &)goto_symextvirtual
symex_with_state(statet &, const get_goto_functiont &, symbol_tablet &)goto_symextvirtual
targetgoto_symextprotected
trigger_auto_object(const exprt &, statet &)goto_symextprotected
validate(const namespacet &ns, const validation_modet vm) constgoto_symextinline
vcc(const exprt &, const std::string &msg, statet &)goto_symextprotectedvirtual
~goto_symext()=defaultgoto_symextvirtual