goto_symext Member List

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

add_memory_leak_checks()	goto_symext
alloc_size_arr_name	goto_symext	protected
analyze_args(const expr2tc &expr)=0	goto_symext	protectedpure virtual
analyze_old_object(const expr2tc &old_obj, type2tc &elem_type, expr2tc &old_base_array, bool &old_is_array)	goto_symext	protected
argument_assignments(const irep_idt &function_identifier, const code_type2t &function_type, const std::vector< expr2tc > &arguments)	goto_symext	protected
argument_value(const type2tc &arg_type, const expr2tc &rhs, const irep_idt &identifier)	goto_symext	protected
art1	goto_symext	protected
assertion(const expr2tc &assertion, const std::string &msg)	goto_symext	protectedvirtual
assertion_message(const namespacet &ns, const goto_programt::instructiont &i)	goto_symext	static
assume(const expr2tc &assumption)	goto_symext	protectedvirtual
assume_loop_continues(const goto_programt::instructiont &instruction, const expr2tc &guard, bool forward, bool always_jumps)	goto_symext	protected
assume_printf_length(const expr2tc &retval, const expr2tc &len)	goto_symext	protected
assume_printf_range(const expr2tc &retval, const BigInt &lo, const BigInt &hi, bool may_fail)	goto_symext	protected
assume_uf_congruence(const irep_idt &identifier, const irep_idt &name, const std::vector< expr2tc > &arguments, const expr2tc &result, const type2tc &ret_type)	goto_symext	protected
base_case	goto_symext	protected
bmct class	goto_symext	friend
bound_dynamic_object_size(const code_assign2t &code)	goto_symext	protected
bounded_loop_truncations	goto_symext	protected
branch_decision_guard(const expr2tc &guard) const	goto_symext	protected
break_insn	goto_symext	protected
build_goto_symex_classes()	goto_symext	friend
bump_call(const code_function_call2t &func_call, const std::string &symname)	goto_symext	protected
calculate_element_count(const expr2tc &size_bytes, const expr2tc &elem_size)	goto_symext	protected
calculate_old_element_count(const expr2tc &old_base_array, const type2tc &elem_type, bool old_is_array)	goto_symext	protected
chase_copies(expr2tc &expr) const	goto_symext
check_incremental(const expr2tc &expr, const std::string &msg)	goto_symext	protected
check_stack_size(const expr2tc &expr, const std::string &subject="")	goto_symext	protected
claim(const expr2tc &expr, const std::string &msg)	goto_symext	protectedvirtual
claim_nonnull_operand(const expr2tc &ptr, const expr2tc &n, const std::string &func)	goto_symext	protected
claim_not_code(const expr2tc &guard)	goto_symext	protected
claim_skips_deferred	goto_symext	protected
claim_valid_operand(const expr2tc &ptr, const expr2tc &n, const std::string &func)	goto_symext	protected
conjunct_indext typedef	goto_symext
copy_definitions	goto_symext	protected
copy_memory_content(const expr2tc &old_base_array, const expr2tc &new_array, const expr2tc &old_elem_count, const expr2tc &new_elem_count, const type2tc &elem_type, bool old_is_array, const guard2tc &guard)	goto_symext	protected
copy_old_objects(const std::list< dereference_callbackt::internal_item > &old_objects, const expr2tc &new_array, const expr2tc &new_elem_count, const type2tc &elem_type, const guard2tc &guard)	goto_symext	protected
copy_single_element(const expr2tc &old_base_array, const expr2tc &new_array, const expr2tc &idx, const type2tc &elem_type, const type2tc &new_elem_type, bool old_is_array, const guard2tc &guard)	goto_symext	protected
create_dynamic_memory_symbol(const type2tc &elem_type, const expr2tc &size_expr, const std::string &name_prefix)	goto_symext	protected
create_result_pointer(const expr2tc &new_array, const type2tc &lhs_type)	goto_symext	protected
cur_state	goto_symext	protected
default_replace_dynamic_allocation(expr2tc &expr)	goto_symext	protected
defer_assumption(const expr2tc &assumption)	goto_symext	protectedvirtual
deferred_assumptions	goto_symext	protected
depth_limit	goto_symext	protected
dereference(expr2tc &expr, dereferencet::modet mode, bool block_assertions=false)	goto_symext	protected
determine_fallback_element_type(const sideeffect2t &code, const expr2tc &lhs)	goto_symext	protected
do_simplify(expr2tc &expr)	goto_symext	protectedvirtual
dyn_info_arr_name	goto_symext	protected
dynamic_memory	goto_symext	protected
dynamic_object_sizes	goto_symext	protected
finalize_realloc_result(const expr2tc &lhs, const expr2tc &result, const expr2tc &new_array, const guard2tc &guard, const expr2tc &realloc_size, const expr2tc &alloc_fail)	goto_symext	protected
first_loop	goto_symext	protected
flush_deferred_assumptions()	goto_symext	protected
format_printf_output(const code_printf2t &call, size_t fmt_idx, printf_formattert &formatter, bool &constant_args)	goto_symext	protected
forward_condition	goto_symext	protected
get_dynamic_counter()=0	goto_symext	protectedpure virtual
get_nondet_counter()=0	goto_symext	protectedpure virtual
get_symex_result()	goto_symext
get_unwind(const symex_targett::sourcet &source, const BigInt &unwind)	goto_symext	protected
get_unwind_recursion(const irep_idt &identifier, BigInt unwind)	goto_symext	protected
goto_functions	goto_symext	protected
goto_symext(const namespacet &_ns, contextt &_new_context, const goto_functionst &goto_functions, std::shared_ptr< symex_targett > _target, optionst &opts)	goto_symext
goto_symext(const goto_symext &sym)	goto_symext
guard_definitions	goto_symext	protected
guard_identifier()	goto_symext	inline
guard_identifier_s	goto_symext	protected
guard_prefix_index	goto_symext	protected
handle_conditional(const expr2tc &lhs, const if2t &if_effect, const guard2tc &guard)	goto_symext	protected
handle_realloc_zero_size(const expr2tc &lhs, const sideeffect2t &code, const guard2tc &guard, const expr2tc &realloc_size)	goto_symext	protected
handle_sideeffect(const expr2tc &lhs, const sideeffect2t &effect, const guard2tc &guard)	goto_symext	protected
inductive_step	goto_symext	protected
internal_deref_items	goto_symext	protected
interval_domain_state	goto_symext	protected
intrinsic_builtin_object_size(const code_function_call2t &func_call, reachability_treet &art)	goto_symext	protected
intrinsic_get_object_size(const code_function_call2t &func_call, reachability_treet &art)	goto_symext	protected
intrinsic_get_thread_data(const code_function_call2t &call, reachability_treet &art)	goto_symext	protected
intrinsic_get_thread_id(const code_function_call2t &call, reachability_treet &art)	goto_symext	protected
intrinsic_havoc_object(const code_function_call2t &call)	goto_symext	protected
intrinsic_init_thread_local(reachability_treet &art)	goto_symext	protected
intrinsic_kill_monitor(reachability_treet &art)	goto_symext	protected
intrinsic_memchr(reachability_treet &art, const code_function_call2t &func_call)	goto_symext	protected
intrinsic_memcmp(reachability_treet &art, const code_function_call2t &func_call)	goto_symext	protected
intrinsic_memcpy(reachability_treet &art, const code_function_call2t &func_call)	goto_symext	protected
intrinsic_memcpy_impl(reachability_treet &art, const code_function_call2t &func_call, const std::string &bump_name)	goto_symext	protected
intrinsic_memmove(reachability_treet &art, const code_function_call2t &func_call)	goto_symext	protected
intrinsic_memset(reachability_treet &art, const code_function_call2t &func_call)	goto_symext	protected
intrinsic_really_atomic_begin(reachability_treet &art)	goto_symext	protected
intrinsic_really_atomic_end(reachability_treet &art)	goto_symext	protected
intrinsic_register_monitor(const code_function_call2t &call, reachability_treet &art)	goto_symext	protected
intrinsic_set_thread_data(const code_function_call2t &call, reachability_treet &art)	goto_symext	protected
intrinsic_spawn_thread(const code_function_call2t &call, reachability_treet &art)	goto_symext	protected
intrinsic_switch_from(reachability_treet &arg)	goto_symext	protected
intrinsic_switch_from_monitor(reachability_treet &art)	goto_symext	protected
intrinsic_switch_to(const code_function_call2t &c, reachability_treet &art)	goto_symext	protected
intrinsic_switch_to_monitor(reachability_treet &art)	goto_symext	protected
intrinsic_terminate_thread(reachability_treet &art)	goto_symext	protected
intrinsic_yield(reachability_treet &arg)	goto_symext	protected
invalidate_object(const expr2tc &ptr)	goto_symext	protected
is_assume_false(const expr2tc &assumption)	goto_symext	protected
is_python_gc_object(const symbolt *base) const	goto_symext	protected
is_valid_object(const symbolt &symbol)	goto_symext	protected
k_induction	goto_symext	protected
key_intrinsic_pointer_reads(const code_function_call2t &call, const irep_idt &id)	goto_symext	protected
loop_bound_exceeded(const expr2tc &guard)	goto_symext	protected
loop_id_to_func_index	goto_symext	protected
make_return_assignment(expr2tc &assign, const expr2tc &code_return)	goto_symext	protected
materialise_old_snapshot(const expr2tc &value, const guard2tc &guard)	goto_symext	protected
max_copy_definition_nodes	goto_symext	protectedstatic
max_unwind	goto_symext	protected
memcmp_resolve_operand(const expr2tc &ptr, unsigned long number_of_bytes, expr2tc &object, uint64_t &offset, uint64_t &avail_bytes, bool rename_object=true)	goto_symext	protected
memcpy_finish(const code_function_call2t &func_call, const expr2tc &dst_arg, const expr2tc &src_arg, const expr2tc &n_arg)	goto_symext	protected
memcpy_symbolic_length(const expr2tc &dst_arg, const expr2tc &src_arg, const expr2tc &n_arg)	goto_symext	protected
memory_leak_check	goto_symext	protected
merge_gotos()	goto_symext	protected
merge_interval_domain(const statet::merge_statet &merge_state)	goto_symext	protected
merge_locality(const statet::merge_statet &merge_state)	goto_symext	protected
merge_value_sets(const statet::merge_statet &merge_state)	goto_symext	protected
model_allocation_failure(const expr2tc &result, const expr2tc &old_ptr, const guard2tc &guard, const expr2tc &over_cap, expr2tc &alloc_fail)	goto_symext	protected
named_object(const expr2tc &base) const	goto_symext	protected
new_context	goto_symext	protected
no_assertions	goto_symext	protected
no_reachable_memleak	goto_symext	protected
no_return_value_opt	goto_symext	protected
no_simplify	goto_symext	protected
no_unwinding_assertions	goto_symext	protected
note_bounded_loop_truncation()	goto_symext	inlineprotectedvirtual
ns	goto_symext	protected
offer_malloc_zero_null(const expr2tc &size, expr2tc &rhs, guard2tc &alloc_guard)	goto_symext	protected
operator=(const goto_symext &sym)	goto_symext
options	goto_symext	protected
partial_loops	goto_symext	protected
path_guard_decides(const expr2tc &new_guard, bool already_false, bool already_true)	goto_symext
phi_function(const statet::merge_statet &merge_state)	goto_symext	protected
pop_frame()	goto_symext	protected
prefix_index(const guard2tc &guard)	goto_symext
printf_output_length(const code_printf2t &call, size_t fmt_idx, size_t &max_len)	goto_symext	protected
printf_return_length(const expr2tc &lhs, const code_printf2t &call, size_t fmt_idx)	goto_symext	protected
propagate_assume_equality(const expr2tc &the_assumption)	goto_symext	protected
reachability_treet class	goto_symext	friend
record_copy_definition(const expr2tc &renamed_lhs, const expr2tc &rhs)	goto_symext
record_frame_alloca(const expr2tc &lhs, const expr2tc &object, bool is_malloc)	goto_symext	protected
record_guard_definition(const expr2tc &guard_expr, const expr2tc &rhs)	goto_symext
record_parked_path(goto_programt::const_targett, statet::merge_state_listt::iterator)	goto_symext	inlineprotectedvirtual
record_property_verdict(const std::string &msg, property_verdictt verdict, const std::string &note="")	goto_symext	protected
recover_va_list_args(const code_printf2t &call, size_t fmt_idx, std::list< expr2tc > &out)	goto_symext	protected
reject_untyped_isinstance(const expr2tc &value)	goto_symext	protected
release_symex_caches()	goto_symext	inline
remaining_claims	goto_symext	protected
replace_dynamic_allocation(expr2tc &expr)	goto_symext	protected
replace_dynamic_size(expr2tc &expr)	goto_symext	protected
replace_nondet(expr2tc &expr)	goto_symext	protected
replace_races_check(expr2tc &expr)	goto_symext	protected
replace_valid_object(expr2tc &expr)	goto_symext	protected
resolve_by_value_set(expr2tc &expr, const expr2tc &ptr, const std::function< expr2tc(const expr2tc &)> &resolve)	goto_symext	protected
resolve_dynamic_size_by_value_set(expr2tc &expr)	goto_symext	protected
resolve_valid_object_by_value_set(expr2tc &expr, const expr2tc &obj_ref)	goto_symext	protected
rewrite_conjunct(const expr2tc &conjunct)	goto_symext
run_builtin(const code_function_call2t &call, const std::string &symname)	goto_symext	protected
run_intrinsic(const code_function_call2t &call, reachability_treet &art, const std::string &symname)	goto_symext	protected
run_next_function_ptr_target(bool first)	goto_symext	protected
simplified_claims	goto_symext	protected
simplify_python_builtins(expr2tc &expr)	goto_symext	protected
snapshot_interval_domain(statet::merge_statet &merge_state)	goto_symext	protected
sprintf_output(const code_printf2t &call, size_t fmt_idx, const type2tc &char_type, std::vector< expr2tc > &chars)	goto_symext	protected
stack_checks_enabled() const	goto_symext	inlineprotected
stack_limit	goto_symext	protected
statet typedef	goto_symext
string_length(const expr2tc &ptr, size_t &max_len)	goto_symext	protected
symex_alloca(const expr2tc &lhs, const sideeffect2t &code, const guard2tc &guard)	goto_symext	protected
symex_asprintf_buffer(const expr2tc &strp, const expr2tc &retval)	goto_symext	protected
symex_assert()	goto_symext	protected
symex_assign(const expr2tc &code, const bool hidden=false, const guard2tc &guard=guard2tc())	goto_symext	protectedvirtual
symex_assign_array(const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)	goto_symext	protected
symex_assign_array_structure(const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)	goto_symext	protected
symex_assign_bitfield(const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)	goto_symext	protected
symex_assign_byte_extract(const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)	goto_symext	protected
symex_assign_concat(const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)	goto_symext	protected
symex_assign_extract(const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)	goto_symext	protected
symex_assign_if(const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)	goto_symext	protected
symex_assign_member(const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)	goto_symext	protected
symex_assign_rec(const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc full_rhs, guard2tc &guard, const bool hidden)	goto_symext	protected
symex_assign_structure(const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)	goto_symext	protected
symex_assign_symbol(const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)	goto_symext	protected
symex_assign_typecast(const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)	goto_symext	protected
symex_assign_union(const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden)	goto_symext	protected
symex_assume()	goto_symext	protected
symex_bounded_math(const code_function_call2t &call, const std::string &function)	goto_symext	protected
symex_cpp_delete(const expr2tc &code)	goto_symext	protected
symex_cpp_new(const expr2tc &lhs, const sideeffect2t &code, const guard2tc &guard)	goto_symext	protected
symex_dead(const expr2tc &code)	goto_symext	protected
symex_decl(const expr2tc &code)	goto_symext	protected
symex_dereference_statet class	goto_symext	friend
symex_end_of_function()	goto_symext	protected
symex_free(const expr2tc &expr)	goto_symext	protected
symex_function_call(const expr2tc &call)	goto_symext	protected
symex_function_call_code(const expr2tc &call)	goto_symext	protectedvirtual
symex_function_call_deref(const expr2tc &call)	goto_symext	protectedvirtual
symex_goto(const expr2tc &old_guard)	goto_symext	protectedvirtual
symex_input(const code_function_call2t &expr)	goto_symext	protected
symex_malloc(const expr2tc &lhs, const sideeffect2t &code, const guard2tc &guard)	goto_symext	protected
symex_mem(const bool is_malloc, const expr2tc &lhs, const sideeffect2t &code, const guard2tc &guard)	goto_symext	protected
symex_mem_inf(const expr2tc &lhs, const type2tc &base_type, const guard2tc &guard)	goto_symext	protected
symex_other(const expr2tc &code)	goto_symext	protected
symex_printf(const expr2tc &lhs, expr2tc &code)	goto_symext	protectedvirtual
symex_realloc(const expr2tc &lhs, const sideeffect2t &code, const guard2tc &guard)	goto_symext	protected
symex_return(const expr2tc &code)	goto_symext	protected
symex_sprintf_store(const code_printf2t &call)	goto_symext	protected
symex_step(reachability_treet &art)	goto_symext	virtual
symex_uninterpreted_function(const code_function_call2t &call, const irep_idt &identifier)	goto_symext	protected
symex_va_arg(const expr2tc &lhs, const sideeffect2t &code, const guard2tc &guard)	goto_symext	protected
symex_witness_assert(expr2tc &new_expr, const std::string &msg)	goto_symext	protected
symex_witness_branching(const expr2tc &old_guard, const expr2tc &new_guard, bool forward, bool &new_guard_true, bool &new_guard_false, const goto_programt::instructiont &instruction)	goto_symext	protected
symex_witness_function_enter(const irep_idt &call_line)	goto_symext	protected
symex_witness_function_return(expr2tc ret_val, const irep_idt &call_line)	goto_symext	protected
target	goto_symext	protected
terminate_handler()	goto_symext	protected
total_claims	goto_symext	protected
total_stack_limit	goto_symext	protected
track_new_pointer(const expr2tc &ptr_obj, const type2tc &new_type, const guard2tc &guard, const expr2tc &size=expr2tc())	goto_symext	protected
uf_applications	goto_symext	protected
unexpected_handler()	goto_symext	protected
unwind_func_set	goto_symext	protected
unwind_set	goto_symext	protected
update_pointer_validity(const expr2tc &old_ptr, const expr2tc &alloc_fail, const guard2tc &guard)	goto_symext	protected
va_copied_from	goto_symext	protected
va_list_copy(const expr2tc &dst, const expr2tc &src)	goto_symext	protected
va_list_cursor(const expr2tc &va_list_expr)	goto_symext	protected
va_list_cursor_symbol(const renaming::level2t::name_record &rec)	goto_symext	protected
va_list_frame(const expr2tc &va_list_expr)	goto_symext	protected
va_list_is_started(const expr2tc &va_list_expr) const	goto_symext	protected
va_list_l1_record(const expr2tc &va_list_expr) const	goto_symext	protected
va_list_mark_started(const expr2tc &va_list_expr, bool started, const expr2tc &cursor)	goto_symext	protected
va_list_owner_records(const expr2tc &va_list_expr) const	goto_symext	protected
va_list_pointee_records(const expr2tc &va_list_expr) const	goto_symext	protected
va_list_start(const expr2tc &va_list_expr)	goto_symext	protected
va_started	goto_symext	protected
valid_ptr_arr_name	goto_symext	protected
validate_witness	goto_symext	protected
value_set_objects(const expr2tc &ptr, bool &complete)	goto_symext	protected
volatile_check(expr2tc &expr)	goto_symext	protected