|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
This is the complete list of members for schedule_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 | schedule_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 | schedule_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 |
| 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 | schedule_execution_statet | inlinevirtual |
| 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 | |
| premaining_claims | schedule_execution_statet | |
| 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 |
| psimplified_claims | schedule_execution_statet | |
| ptotal_claims | schedule_execution_statet | |
| ptruncations | schedule_execution_statet | |
| 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 ¬e="") | 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 |
| schedule_execution_statet(const goto_functionst &goto_functions, const namespacet &ns, reachability_treet *art, std::shared_ptr< symex_targett > _target, contextt &context, optionst &options, unsigned int *ptotal_claims, unsigned int *premaining_claims, unsigned int *psimplified_claims, unsigned int *ptruncations) | schedule_execution_statet | inline |
| schedule_execution_statet(const schedule_execution_statet &ref)=default | schedule_execution_statet | |
| 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 |
| ~execution_statet()=default | execution_statet | virtual |
| ~schedule_execution_statet() override | schedule_execution_statet |