cprover
goto_symext Member List

This is the complete list of members for goto_symext, 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 &, statet &, guardt &, bool keep_array)goto_symextprotected
allow_pointer_unsoundnessgoto_symextprotected
assignment_typet typedefgoto_symextprotected
atomic_section_countergoto_symextprotected
build_symex_nondet(typet &type)goto_symextprotected
clean_expr(exprt &, statet &, bool write)goto_symextprotected
constant_propagationgoto_symext
dereference(exprt &, statet &, const bool write)goto_symextprotectedvirtual
dereference_rec(exprt &, statet &, guardt &, const bool write)goto_symextprotected
dereference_rec_address_of(exprt &, statet &, guardt &)goto_symextprotected
do_simplify(exprt &)goto_symextprotectedvirtual
doing_path_explorationgoto_symextprotected
dynamic_countergoto_symextprotectedstatic
get_goto_functiont typedefgoto_symext
get_unwind(const symex_targett::sourcet &source, unsigned unwind)goto_symextprotectedvirtual
get_unwind_recursion(const irep_idt &identifier, const 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, 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
max_depthgoto_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 &identifier)goto_symextinlineprotectedvirtual
nondet_countgoto_symextprotectedstatic
nsgoto_symextprotected
optionsgoto_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_storagegoto_symextprotected
phi_function(const statet::goto_statet &goto_state, statet &)goto_symextprotected
pop_frame(statet &)goto_symextprotected
process_array_expr(exprt &)goto_symextprotected
read(exprt &)goto_symextprotected
remaining_vccsgoto_symext
replace_nondet(exprt &)goto_symextprotected
resume_symex_from_saved_state(const get_goto_functiont &get_goto_function, const statet &saved_state, symex_target_equationt *const saved_equation, symbol_tablet &new_symbol_table)goto_symextvirtual
return_assignment(statet &)goto_symextprotected
rewrite_quantifiers(exprt &, statet &)goto_symextprotected
self_loops_to_assumptionsgoto_symext
should_pause_symexgoto_symext
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_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 goto_functionst &goto_functions, symbol_tablet &new_symbol_table)goto_symextvirtual
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_instruction_range(statet &, const goto_functionst &, goto_programt::const_targett first, goto_programt::const_targett limit)goto_symextvirtual
symex_instruction_range(statet &state, const get_goto_functiont &get_goto_function, goto_programt::const_targett first, goto_programt::const_targett limit)goto_symextvirtual
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 &lhs, const exprt &rhs)goto_symextprotectedvirtual
symex_start_thread(statet &)goto_symextprotectedvirtual
symex_step(const get_goto_functiont &, statet &)goto_symextprotectedvirtual
symex_step_goto(statet &, bool taken)goto_symextvirtual
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_transition(statet &, goto_programt::const_targett to, bool is_backwards_goto=false)goto_symextprotectedvirtual
symex_transition(statet &state)goto_symextinlineprotectedvirtual
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
total_vccsgoto_symext
trigger_auto_object(const exprt &, statet &)goto_symextprotected
vcc(const exprt &, const std::string &msg, statet &)goto_symextprotectedvirtual
~goto_symext()goto_symextinlinevirtual