cprover
|
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_symext | protected |
add_to_lhs(const exprt &lhs, const exprt &what) | goto_symext | protectedstatic |
address_arithmetic(const exprt &, statet &, guardt &, bool keep_array) | goto_symext | protected |
allow_pointer_unsoundness | goto_symext | protected |
assignment_typet typedef | goto_symext | protected |
atomic_section_counter | goto_symext | protected |
build_symex_nondet(typet &type) | goto_symext | protected |
clean_expr(exprt &, statet &, bool write) | goto_symext | protected |
constant_propagation | goto_symext | |
dereference(exprt &, statet &, const bool write) | goto_symext | protectedvirtual |
dereference_rec(exprt &, statet &, guardt &, const bool write) | goto_symext | protected |
dereference_rec_address_of(exprt &, statet &, guardt &) | goto_symext | protected |
do_simplify(exprt &) | goto_symext | protectedvirtual |
doing_path_exploration | goto_symext | protected |
dynamic_counter | goto_symext | protectedstatic |
get_goto_functiont typedef | goto_symext | |
get_unwind(const symex_targett::sourcet &source, unsigned unwind) | goto_symext | protectedvirtual |
get_unwind_recursion(const irep_idt &identifier, const unsigned thread_nr, unsigned unwind) | goto_symext | protectedvirtual |
goto_symext(message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage) | goto_symext | inline |
guard_identifier | goto_symext | protected |
havoc_rec(statet &, const guardt &, const exprt &) | goto_symext | protected |
initialize_auto_object(const exprt &, statet &) | goto_symext | protected |
initialize_entry_point(statet &state, const get_goto_functiont &get_goto_function, goto_programt::const_targett pc, goto_programt::const_targett limit) | goto_symext | protected |
is_index_member_symbol_if(const exprt &expr) | goto_symext | protectedstatic |
language_mode | goto_symext | |
locality(const irep_idt function_identifier, statet &, const goto_functionst::goto_functiont &) | goto_symext | protected |
log | goto_symext | mutableprotected |
loop_bound_exceeded(statet &, const exprt &guard) | goto_symext | protectedvirtual |
make_auto_object(const typet &, statet &) | goto_symext | protected |
max_depth | goto_symext | protected |
merge_goto(const statet::goto_statet &goto_state, statet &) | goto_symext | protectedvirtual |
merge_gotos(statet &) | goto_symext | protected |
merge_value_sets(const statet::goto_statet &goto_state, statet &dest) | goto_symext | protected |
no_body(const irep_idt &identifier) | goto_symext | inlineprotectedvirtual |
nondet_count | goto_symext | protectedstatic |
ns | goto_symext | protected |
options | goto_symext | protected |
outer_symbol_table | goto_symext | protected |
parameter_assignments(const irep_idt function_identifier, const goto_functionst::goto_functiont &, statet &, const exprt::operandst &arguments) | goto_symext | protected |
path_storage | goto_symext | protected |
phi_function(const statet::goto_statet &goto_state, statet &) | goto_symext | protected |
pop_frame(statet &) | goto_symext | protected |
process_array_expr(exprt &) | goto_symext | protected |
read(exprt &) | goto_symext | protected |
remaining_vccs | goto_symext | |
replace_nondet(exprt &) | goto_symext | protected |
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_symext | virtual |
return_assignment(statet &) | goto_symext | protected |
rewrite_quantifiers(exprt &, statet &) | goto_symext | protected |
self_loops_to_assumptions | goto_symext | |
should_pause_symex | goto_symext | |
statet typedef | goto_symext | |
symex_allocate(statet &, const exprt &lhs, const side_effect_exprt &) | goto_symext | protectedvirtual |
symex_assign(statet &, const code_assignt &) | goto_symext | protected |
symex_assign_array(statet &, const index_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet) | goto_symext | protected |
symex_assign_byte_extract(statet &, const byte_extract_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet) | goto_symext | protected |
symex_assign_if(statet &, const if_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet) | goto_symext | protected |
symex_assign_rec(statet &, const exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet) | goto_symext | protected |
symex_assign_struct_member(statet &, const member_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet) | goto_symext | protected |
symex_assign_symbol(statet &, const ssa_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet) | goto_symext | protected |
symex_assign_typecast(statet &, const typecast_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet) | goto_symext | protected |
symex_assume(statet &, const exprt &cond) | goto_symext | protectedvirtual |
symex_atomic_begin(statet &) | goto_symext | protectedvirtual |
symex_atomic_end(statet &) | goto_symext | protectedvirtual |
symex_catch(statet &) | goto_symext | protected |
symex_cpp_delete(statet &, const codet &) | goto_symext | protectedvirtual |
symex_cpp_new(statet &, const exprt &lhs, const side_effect_exprt &) | goto_symext | protectedvirtual |
symex_dead(statet &) | goto_symext | protectedvirtual |
symex_decl(statet &) | goto_symext | protectedvirtual |
symex_decl(statet &, const symbol_exprt &expr) | goto_symext | protectedvirtual |
symex_dereference_statet class | goto_symext | friend |
symex_end_of_function(statet &) | goto_symext | protectedvirtual |
symex_fkt(statet &, const code_function_callt &) | goto_symext | protectedvirtual |
symex_from_entry_point_of(const goto_functionst &goto_functions, symbol_tablet &new_symbol_table) | goto_symext | virtual |
symex_from_entry_point_of(const get_goto_functiont &get_goto_function, symbol_tablet &new_symbol_table) | goto_symext | virtual |
symex_function_call(const get_goto_functiont &, statet &, const code_function_callt &) | goto_symext | protectedvirtual |
symex_function_call_code(const get_goto_functiont &, statet &, const code_function_callt &) | goto_symext | protectedvirtual |
symex_function_call_symbol(const get_goto_functiont &, statet &, const code_function_callt &) | goto_symext | protectedvirtual |
symex_gcc_builtin_va_arg_next(statet &, const exprt &lhs, const side_effect_exprt &) | goto_symext | protectedvirtual |
symex_goto(statet &) | goto_symext | protectedvirtual |
symex_input(statet &, const codet &) | goto_symext | protectedvirtual |
symex_instruction_range(statet &, const goto_functionst &, goto_programt::const_targett first, goto_programt::const_targett limit) | goto_symext | virtual |
symex_instruction_range(statet &state, const get_goto_functiont &get_goto_function, goto_programt::const_targett first, goto_programt::const_targett limit) | goto_symext | virtual |
symex_macro(statet &, const code_function_callt &) | goto_symext | protectedvirtual |
symex_other(statet &) | goto_symext | protectedvirtual |
symex_output(statet &, const codet &) | goto_symext | protectedvirtual |
symex_printf(statet &, const exprt &lhs, const exprt &rhs) | goto_symext | protectedvirtual |
symex_start_thread(statet &) | goto_symext | protectedvirtual |
symex_step(const get_goto_functiont &, statet &) | goto_symext | protectedvirtual |
symex_step_goto(statet &, bool taken) | goto_symext | virtual |
symex_threaded_step(statet &, const get_goto_functiont &) | goto_symext | protected |
symex_throw(statet &) | goto_symext | protected |
symex_trace(statet &, const code_function_callt &) | goto_symext | protectedvirtual |
symex_transition(statet &, goto_programt::const_targett to, bool is_backwards_goto=false) | goto_symext | protectedvirtual |
symex_transition(statet &state) | goto_symext | inlineprotectedvirtual |
symex_with_state(statet &, const goto_functionst &, symbol_tablet &) | goto_symext | virtual |
symex_with_state(statet &, const get_goto_functiont &, symbol_tablet &) | goto_symext | virtual |
target | goto_symext | protected |
total_vccs | goto_symext | |
trigger_auto_object(const exprt &, statet &) | goto_symext | protected |
vcc(const exprt &, const std::string &msg, statet &) | goto_symext | protectedvirtual |
~goto_symext() | goto_symext | inlinevirtual |