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 &expr, statet &state, guardt &guard, bool keep_array) | goto_symext | protected |
assignment_typet typedef | goto_symext | protected |
atomic_section_counter | goto_symext | protected |
clean_expr(exprt &expr, statet &state, bool write) | goto_symext | protected |
constant_propagation | goto_symext | |
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 |
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(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 | |
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 |
make_auto_object(const typet &type) | goto_symext | protected |
merge_goto(const statet::goto_statet &goto_state, statet &state) | goto_symext | protectedvirtual |
merge_gotos(statet &state) | goto_symext | protected |
merge_value_sets(const statet::goto_statet &goto_state, statet &dest) | goto_symext | protected |
new_name(symbolt &symbol) | goto_symext | protected |
new_symbol_table | goto_symext | |
no_body(const irep_idt &identifier) | goto_symext | inlineprotectedvirtual |
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 | |
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 |
read(exprt &expr) | goto_symext | protected |
remaining_vccs | goto_symext | |
replace_array_equal(exprt &expr) | goto_symext | protected |
replace_nondet(exprt &expr) | goto_symext | protected |
return_assignment(statet &state) | goto_symext | protected |
rewrite_quantifiers(exprt &expr, statet &state) | goto_symext | protected |
statet typedef | goto_symext | |
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_catch(statet &state) | goto_symext | 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_dereference_statet class | goto_symext | friend |
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) | goto_symext | virtual |
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 |
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 |
~goto_symext() | goto_symext | inlinevirtual |