symex_bmc_incremental_one_loopt Member List

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

_remaining_vccs	goto_symext	protected
_total_vccs	goto_symext	protected
add_loop_unwind_handler(loop_unwind_handlert handler)	symex_bmct	inline
add_recursion_unwind_handler(recursion_unwind_handlert handler)	symex_bmct	inline
address_arithmetic(const exprt &, statet &, bool keep_array)	goto_symext	protected
apply_goto_condition(goto_symex_statet &current_state, goto_statet &jump_taken_state, goto_statet &jump_not_taken_state, const exprt &original_guard, const exprt &new_guard, const namespacet &ns)	goto_symext	protected
assign_string_constant(statet &state, symex_assignt &symex_assign, const ssa_exprt &length, const constant_exprt &new_length, const ssa_exprt &char_array, const array_exprt &new_char_array)	goto_symext	protected
assignment_typet typedef	goto_symext	protected
associate_array_to_pointer(statet &state, symex_assignt &symex_assign, const array_exprt &new_char_array, const address_of_exprt &string_data)	goto_symext	protected
atomic_section_counter	goto_symext	protected
cache_dereference(exprt &dereference_result, statet &state)	goto_symext	protected
check_break(const irep_idt &loop_id, unsigned unwind) override	symex_bmc_incremental_one_loopt	protectedvirtual
clean_expr(exprt expr, statet &state, bool write)	goto_symext	protected
complexity_module	goto_symext	protected
constant_propagate_assignment_with_side_effects(statet &state, symex_assignt &symex_assign, const exprt &lhs, const exprt &rhs)	goto_symext	protected
constant_propagate_case_change(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1, bool to_upper)	goto_symext	protected
constant_propagate_delete(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)	goto_symext	protected
constant_propagate_delete_char_at(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)	goto_symext	protected
constant_propagate_empty_string(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)	goto_symext	protected
constant_propagate_integer_to_string(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)	goto_symext	protected
constant_propagate_replace(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)	goto_symext	protected
constant_propagate_set_char_at(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)	goto_symext	protected
constant_propagate_set_length(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)	goto_symext	protected
constant_propagate_string_concat(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)	goto_symext	protected
constant_propagate_string_substring(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)	goto_symext	protected
constant_propagate_trim(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)	goto_symext	protected
dereference(exprt &, statet &, bool write)	goto_symext	protectedvirtual
dereference_rec(exprt &expr, statet &state, bool write, bool is_in_quantifier)	goto_symext	protected
do_simplify(exprt &expr)	goto_symext	protectedvirtual
execute_next_instruction(const get_goto_functiont &get_goto_function, statet &state)	goto_symext	protected
from_entry_point_of(const get_goto_functiont &get_goto_function, symbol_tablet &new_symbol_table)	symex_bmc_incremental_one_loopt
get_goto_function(abstract_goto_modelt &goto_model)	goto_symext	static
get_goto_functiont typedef	goto_symext
get_new_string_data_symbol(statet &state, symex_assignt &symex_assign, const std::string &aux_symbol_name, const ssa_exprt &char_array, const array_exprt &new_char_array)	goto_symext	protected
get_remaining_vccs() const	goto_symext	inline
get_total_vccs() const	goto_symext	inline
get_unwind_recursion(const irep_idt &identifier, unsigned thread_nr, unsigned unwind) override	symex_bmct	protectedvirtual
goto_symext(message_handlert &mh, const symbol_table_baset &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage, guard_managert &guard_manager)	goto_symext	inline
guard_manager	goto_symext	protected
havoc_rec(statet &state, const guardt &guard, const exprt &dest)	goto_symext	protected
ignore_assertions	goto_symext
incr_loop_id	symex_bmc_incremental_one_loopt	protected
incr_max_unwind	symex_bmc_incremental_one_loopt	protected
incr_min_unwind	symex_bmc_incremental_one_loopt	protected
initialize_auto_object(const exprt &, statet &)	goto_symext	protected
initialize_entry_point_state(const get_goto_functiont &get_goto_function)	goto_symext	protected
initialize_path_storage_from_entry_point_of(const get_goto_functiont &get_goto_function, symbol_table_baset &new_symbol_table, const shadow_memory_field_definitionst &fields)	goto_symext	virtual
instruction_local_symbols	goto_symext	protected
kill_instruction_local_symbols(statet &state)	goto_symext	protected
language_mode	goto_symext
last_source_location	symex_bmct
lift_let(statet &state, const let_exprt &let_expr)	goto_symext	protected
lift_lets(statet &, exprt &)	goto_symext	protected
locality(const irep_idt &function_identifier, goto_symext::statet &state, const goto_functionst::goto_functiont &goto_function)	goto_symext	protectedvirtual
log	goto_symext	mutableprotected
log_unwinding(unsigned unwind)	symex_bmc_incremental_one_loopt	protected
loop_bound_exceeded(statet &state, const exprt &guard)	goto_symext	protectedvirtual
loop_unwind_handlers	symex_bmct	protected
loop_unwind_handlert typedef	symex_bmct
make_auto_object(const typet &, statet &)	goto_symext	protected
merge_goto(const symex_targett::sourcet &source, goto_statet &&goto_state, statet &state) override	symex_bmct	protectedvirtual
merge_gotos(statet &state)	goto_symext	protected
ns	goto_symext	protected
outer_symbol_table	goto_symext	protected
output_coverage_report(const goto_functionst &goto_functions, const std::string &path) const	symex_bmct	inline
output_ui	symex_bmc_incremental_one_loopt	protected
parameter_assignments(const irep_idt &function_identifier, const goto_functionst::goto_functiont &goto_function, statet &state, const exprt::operandst &arguments)	goto_symext	protected
path_segment_vccs	goto_symext
path_storage	goto_symext	protected
phi_function(const goto_statet &goto_state, statet &dest_state)	goto_symext	protected
print_callstack_entry(const symex_targett::sourcet &target)	goto_symext	protected
print_symex_step(statet &state)	goto_symext	protected
process_array_expr(statet &, exprt &)	goto_symext	protected
record_coverage	symex_bmct
recursion_unwind_handlers	symex_bmct	protected
recursion_unwind_handlert typedef	symex_bmct
resume(const get_goto_functiont &get_goto_function)	symex_bmc_incremental_one_loopt
resume_symex_from_saved_state(const get_goto_functiont &get_goto_function, const statet &saved_state, symex_target_equationt *saved_equation)	goto_symext	virtual
rewrite_quantifiers(exprt &, statet &)	goto_symext	protected
shadow_memory	goto_symext	protected
should_pause_symex	goto_symext
should_stop_unwind(const symex_targett::sourcet &source, const call_stackt &context, unsigned unwind) override	symex_bmc_incremental_one_loopt	protectedvirtual
state	symex_bmc_incremental_one_loopt	protected
statet typedef	goto_symext
symex_allocate(statet &state, const exprt &lhs, const side_effect_exprt &code)	goto_symext	protectedvirtual
symex_assert(const goto_programt::instructiont &, statet &)	goto_symext	protected
symex_assign(statet &state, const exprt &lhs, const exprt &rhs)	goto_symext	protected
symex_assume(statet &state, const exprt &cond)	goto_symext	protectedvirtual
symex_assume_l2(statet &, const exprt &cond)	goto_symext	protected
symex_atomic_begin(statet &state)	goto_symext	protectedvirtual
symex_atomic_end(statet &state)	goto_symext	protectedvirtual
symex_bmc_incremental_one_loopt(message_handlert &, const symbol_tablet &outer_symbol_table, symex_target_equationt &, const optionst &, path_storaget &, guard_managert &, unwindsett &, ui_message_handlert::uit output_ui)	symex_bmc_incremental_one_loopt
symex_bmct(message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage, guard_managert &guard_manager, unwindsett &unwindset)	symex_bmct
symex_catch(statet &state)	goto_symext	protected
symex_config	goto_symext	protected
symex_coverage	symex_bmct	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_dead(statet &state, const symbol_exprt &symbol_expr)	goto_symext	protected
symex_decl(statet &state)	goto_symext	protectedvirtual
symex_decl(statet &state, const symbol_exprt &expr)	goto_symext	protectedvirtual
symex_end_of_function(statet &)	goto_symext	protectedvirtual
symex_from_entry_point_of(const get_goto_functiont &get_goto_function, const shadow_memory_field_definitionst &fields)	goto_symext	virtual
symex_function_call(const get_goto_functiont &get_goto_function, statet &state, const goto_programt::instructiont &instruction)	goto_symext	protectedvirtual
symex_function_call_post_clean(const get_goto_functiont &get_goto_function, statet &state, const exprt &cleaned_lhs, const symbol_exprt &function, const exprt::operandst &cleaned_arguments)	goto_symext	protectedvirtual
symex_function_call_symbol(const get_goto_functiont &get_goto_function, statet &state, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments)	goto_symext	protectedvirtual
symex_goto(statet &state)	goto_symext	protectedvirtual
symex_input(statet &state, const codet &code)	goto_symext	protectedvirtual
symex_other(statet &state)	goto_symext	protectedvirtual
symex_output(statet &state, const codet &code)	goto_symext	protectedvirtual
symex_printf(statet &state, const exprt &rhs)	goto_symext	protectedvirtual
symex_set_return_value(statet &state, const exprt &return_value)	goto_symext	protected
symex_start_thread(statet &state)	goto_symext	protectedvirtual
symex_step(const get_goto_functiont &get_goto_function, statet &state) override	symex_bmct	protectedvirtual
symex_threaded_step(statet &state, const get_goto_functiont &get_goto_function)	goto_symext	protected
symex_throw(statet &state)	goto_symext	protected
symex_unreachable_goto(statet &state)	goto_symext	protected
symex_va_start(statet &, const exprt &lhs, const side_effect_exprt &)	goto_symext	protectedvirtual
symex_with_state(statet &state, const get_goto_functiont &get_goto_functions)	goto_symext	virtual
target	goto_symext	protected
trigger_auto_object(const exprt &, statet &)	goto_symext	protected
try_evaluate_constant(const statet &state, const exprt &expr)	goto_symext	protectedstatic
try_evaluate_constant_string(const statet &state, const exprt &content)	goto_symext	protected
try_filter_value_sets(goto_symex_statet &state, exprt condition, const value_sett &original_value_set, value_sett *jump_taken_value_set, value_sett *jump_not_taken_value_set, const namespacet &ns)	goto_symext	protected
unwindset	symex_bmct
validate(const validation_modet vm) const	goto_symext	inline
vcc(const exprt &cond, const irep_idt &property_id, const std::string &msg, statet &state)	goto_symext	protectedvirtual
~goto_symext()=default	goto_symext	virtual