dfs_execution_statet Member List

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

access_kindt enum name	execution_statet
active_thread	execution_statet
add_memory_leak_checks()	goto_symext
add_thread(const goto_programt *prog)	execution_statet
all_threads_terminal() const	execution_statet
alloc_size_arr_name	goto_symext	protected
analyze_args(const expr2tc &expr) override	execution_statet	virtual
analyze_assign(const expr2tc &assign)	execution_statet
analyze_old_object(const expr2tc &old_obj, type2tc &elem_type, expr2tc &old_base_array, bool &old_is_array)	goto_symext	protected
analyze_read(const expr2tc &expr)	execution_statet
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) override	execution_statet	virtual
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
atomic_numbers	execution_statet
base_case	goto_symext	protected
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
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_mpor_constraints()	execution_statet
calculate_old_element_count(const expr2tc &old_base_array, const type2tc &elem_type, bool old_is_array)	goto_symext	protected
can_execution_continue() const	execution_statet
chase_copies(expr2tc &expr) const	goto_symext
check_if_ileaves_blocked()	execution_statet
check_incremental(const expr2tc &expr, const std::string &msg)	goto_symext	protected
check_mpor_dependency(unsigned int j, unsigned int l) const	execution_statet
check_mpor_dependency(unsigned int j, const transition_footprintt &fp) const	execution_statet
check_stack_size(const expr2tc &expr, const std::string &subject="")	goto_symext	protected
claim(const expr2tc &expr, const std::string &msg) override	execution_statet	virtual
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
clone() const override	dfs_execution_statet	virtual
conjunct_indext typedef	goto_symext
copy_definitions	goto_symext	protected
copy_derived_from(const execution_statet &ex)	execution_statet	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
CS_number	execution_statet	protected
cswitch_forced	execution_statet	protected
cull_all_paths()	execution_statet
cur_state	goto_symext	protected
decrement_active_atomic_number()	execution_statet
default_replace_dynamic_allocation(expr2tc &expr)	goto_symext	protected
defer_assumption(const expr2tc &assumption) override	execution_statet	virtual
deferred_assumptions	goto_symext	protected
dependency_chain	execution_statet	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
dfs_execution_statet(const goto_functionst &goto_functions, const namespacet &ns, reachability_treet *art, std::shared_ptr< symex_targett > _target, contextt &context, optionst &options)	dfs_execution_statet	inline
dfs_execution_statet(const dfs_execution_statet &ref)=default	dfs_execution_statet
do_simplify(expr2tc &expr)	goto_symext	protectedvirtual
dyn_info_arr_name	goto_symext	protected
dynamic_counter	execution_statet	thread_localstatic
dynamic_memory	goto_symext	protected
dynamic_object_sizes	goto_symext	protected
end_thread()	execution_statet
execute_guard()	execution_statet
execution_statet(const goto_functionst &goto_functions, const namespacet &ns, reachability_treet *art, std::shared_ptr< symex_targett > _target, contextt &context, std::shared_ptr< ex_state_level2t > l2init, optionst &options)	execution_statet
execution_statet(const execution_statet &ex)	execution_statet
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
force_cswitch()	execution_statet	inline
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
generate_hash() const	execution_statet
get_active_atomic_number() const	execution_statet
get_active_state()	execution_statet
get_active_state() const	execution_statet
get_active_state_number() const	execution_statet	inline
get_context_switch() const	execution_statet	inline
get_dependency_chain() const	execution_statet	inline
get_dynamic_counter() override	execution_statet	virtual
get_expr_globals(const namespacet &ns, const expr2tc &expr, std::set< expr2tc > &global_list, access_kindt kind, bool under_deref=false)	execution_statet
get_guard_identifier()	execution_statet
get_nondet_counter() override	execution_statet	virtual
get_symex_result()	goto_symext
get_thread_last_transition() const	execution_statet	inline
get_thread_start_data(unsigned int tid) const	execution_statet	inline
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
global_value_set	execution_statet
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_execution	execution_statet
guard_execution_name	execution_statet	static
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
has_cswitch_point_occured() const	execution_statet
increment_active_atomic_number()	execution_statet
increment_context_switch()	execution_statet	inline
inductive_step	goto_symext	protected
interleaving_unviable	execution_statet
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_cur_state_guard_false(const expr2tc &guard)	execution_statet
is_python_gc_object(const symbolt *base) const	goto_symext	protected
is_transition_blocked_by_mpor() const	execution_statet	inline
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
kill_monitor_thread()	execution_statet
last_active_thread	execution_statet
last_transition	execution_statet
last_transition_footprint(unsigned int tid) const	execution_statet	inline
loop_bound_exceeded(const expr2tc &guard)	goto_symext	protected
loop_id_to_func_index	goto_symext	protected
main_returned	execution_statet
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_statet typedef	execution_statet
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
mon_from_tid	execution_statet
monitor_from_tid	execution_statet
monitor_tid	execution_statet
mpor_says_no	execution_statet	protected
named_object(const expr2tc &base) const	goto_symext	protected
new_context	goto_symext	protected
no_assertions	goto_symext	protected
no_propagation	execution_statet	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
node_count	execution_statet	thread_localstatic
node_id	execution_statet
nondet_count	execution_statet
note_bounded_loop_truncation() override	execution_statet	virtual
ns	goto_symext	protected
offer_malloc_zero_null(const expr2tc &size, expr2tc &rhs, guard2tc &alloc_guard)	goto_symext	protected
operator=(const execution_statet &ex)=delete	execution_statet
goto_symext::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
preserve_last_paths(const transition_resultt &transition)	execution_statet
preserved_paths	execution_statet
print_stack_traces(unsigned int indent=0) const	execution_statet
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
record_access_key(const expr2tc &key, std::set< expr2tc > &global_list, access_kindt kind)	execution_statet
record_aggregate_held_target(const namespacet &ns, const expr2tc &expr, std::set< expr2tc > &global_list, access_kindt kind)	execution_statet
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 target, statet::merge_state_listt::iterator parked) override	execution_statet	virtual
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
reset_dynamic_counter()	execution_statet	static
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_pointer_target(const namespacet &ns, const expr2tc &ptr, bool &to_global, bool through_deref)	execution_statet
resolve_valid_object_by_value_set(expr2tc &expr, const expr2tc &obj_ref)	goto_symext	protected
restore_last_paths()	execution_statet
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
set_thread_start_data(unsigned int tid, const expr2tc &argdata)	execution_statet	inline
simplified_claims	goto_symext	protected
simplify_python_builtins(expr2tc &expr)	goto_symext	protected
smt_during_symex	execution_statet	protected
smt_thread_guard	execution_statet	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
state_level2	execution_statet
statet typedef	goto_symext
string_length(const expr2tc &ptr, size_t &max_len)	goto_symext	protected
switch_away_from_monitor()	execution_statet
switch_to_monitor()	execution_statet
switch_to_thread(unsigned int i)	execution_statet
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, const guard2tc &guard) override	execution_statet	virtual
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_end_function(reachability_treet &art, const goto_programt::instructiont &instruction)	execution_statet
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) override	execution_statet	virtual
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) override	execution_statet	virtual
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) override	execution_statet	virtual
symex_trace	execution_statet	protected
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
thread_cswitch_threshold	execution_statet
thread_last_reads	execution_statet	protected
thread_last_transition	execution_statet	protected
thread_last_writes	execution_statet	protected
thread_start_data	execution_statet
threads_state	execution_statet
tid_is_set	execution_statet
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
transition_ordinal	execution_statet	protected
uf_applications	goto_symext	protected
unexpected_handler()	goto_symext	protected
unwind_func_set	goto_symext	protected
unwind_set	goto_symext	protected
update_after_switch_point()	execution_statet
update_hash_for_assignment(const expr2tc &rhs)	execution_statet
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
~dfs_execution_statet() override	dfs_execution_statet
~execution_statet()=default	execution_statet	virtual