CBMC
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_vccsgoto_symextprotected
_total_vccsgoto_symextprotected
add_loop_unwind_handler(loop_unwind_handlert handler)symex_bmctinline
add_recursion_unwind_handler(recursion_unwind_handlert handler)symex_bmctinline
address_arithmetic(const exprt &, statet &, bool keep_array)goto_symextprotected
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_symextprotected
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_symextprotected
assignment_typet typedefgoto_symextprotected
associate_array_to_pointer(statet &state, symex_assignt &symex_assign, const array_exprt &new_char_array, const address_of_exprt &string_data)goto_symextprotected
atomic_section_countergoto_symextprotected
cache_dereference(exprt &dereference_result, statet &state)goto_symextprotected
check_break(const irep_idt &loop_id, unsigned unwind) overridesymex_bmc_incremental_one_looptprotectedvirtual
clean_expr(exprt expr, statet &state, bool write)goto_symextprotected
complexity_modulegoto_symextprotected
constant_propagate_assignment_with_side_effects(statet &state, symex_assignt &symex_assign, const exprt &lhs, const exprt &rhs)goto_symextprotected
constant_propagate_case_change(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1, bool to_upper)goto_symextprotected
constant_propagate_delete(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)goto_symextprotected
constant_propagate_delete_char_at(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)goto_symextprotected
constant_propagate_empty_string(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)goto_symextprotected
constant_propagate_integer_to_string(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)goto_symextprotected
constant_propagate_replace(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)goto_symextprotected
constant_propagate_set_char_at(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)goto_symextprotected
constant_propagate_set_length(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)goto_symextprotected
constant_propagate_string_concat(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)goto_symextprotected
constant_propagate_string_substring(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)goto_symextprotected
constant_propagate_trim(statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1)goto_symextprotected
dereference(exprt &, statet &, bool write)goto_symextprotectedvirtual
dereference_rec(exprt &expr, statet &state, bool write, bool is_in_quantifier)goto_symextprotected
do_simplify(exprt &expr)goto_symextprotectedvirtual
execute_next_instruction(const get_goto_functiont &get_goto_function, statet &state)goto_symextprotected
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_symextstatic
get_goto_functiont typedefgoto_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_symextprotected
get_remaining_vccs() constgoto_symextinline
get_total_vccs() constgoto_symextinline
get_unwind_recursion(const irep_idt &identifier, unsigned thread_nr, unsigned unwind) overridesymex_bmctprotectedvirtual
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_symextinline
guard_managergoto_symextprotected
havoc_rec(statet &state, const guardt &guard, const exprt &dest)goto_symextprotected
ignore_assertionsgoto_symext
incr_loop_idsymex_bmc_incremental_one_looptprotected
incr_max_unwindsymex_bmc_incremental_one_looptprotected
incr_min_unwindsymex_bmc_incremental_one_looptprotected
initialize_auto_object(const exprt &, statet &)goto_symextprotected
initialize_entry_point_state(const get_goto_functiont &get_goto_function)goto_symextprotected
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_symextvirtual
instruction_local_symbolsgoto_symextprotected
kill_instruction_local_symbols(statet &state)goto_symextprotected
language_modegoto_symext
last_source_locationsymex_bmct
lift_let(statet &state, const let_exprt &let_expr)goto_symextprotected
lift_lets(statet &, exprt &)goto_symextprotected
locality(const irep_idt &function_identifier, goto_symext::statet &state, const goto_functionst::goto_functiont &goto_function)goto_symextprotectedvirtual
loggoto_symextmutableprotected
log_unwinding(unsigned unwind)symex_bmc_incremental_one_looptprotected
loop_bound_exceeded(statet &state, const exprt &guard)goto_symextprotectedvirtual
loop_unwind_handlerssymex_bmctprotected
loop_unwind_handlert typedefsymex_bmct
make_auto_object(const typet &, statet &)goto_symextprotected
merge_goto(const symex_targett::sourcet &source, goto_statet &&goto_state, statet &state) overridesymex_bmctprotectedvirtual
merge_gotos(statet &state)goto_symextprotected
nsgoto_symextprotected
outer_symbol_tablegoto_symextprotected
output_coverage_report(const goto_functionst &goto_functions, const std::string &path) constsymex_bmctinline
output_uisymex_bmc_incremental_one_looptprotected
parameter_assignments(const irep_idt &function_identifier, const goto_functionst::goto_functiont &goto_function, statet &state, const exprt::operandst &arguments)goto_symextprotected
path_segment_vccsgoto_symext
path_storagegoto_symextprotected
phi_function(const goto_statet &goto_state, statet &dest_state)goto_symextprotected
print_callstack_entry(const symex_targett::sourcet &target)goto_symextprotected
print_symex_step(statet &state)goto_symextprotected
process_array_expr(statet &, exprt &)goto_symextprotected
record_coveragesymex_bmct
recursion_unwind_handlerssymex_bmctprotected
recursion_unwind_handlert typedefsymex_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_symextvirtual
rewrite_quantifiers(exprt &, statet &)goto_symextprotected
shadow_memorygoto_symextprotected
should_pause_symexgoto_symext
should_stop_unwind(const symex_targett::sourcet &source, const call_stackt &context, unsigned unwind) overridesymex_bmc_incremental_one_looptprotectedvirtual
statesymex_bmc_incremental_one_looptprotected
statet typedefgoto_symext
symex_allocate(statet &state, const exprt &lhs, const side_effect_exprt &code)goto_symextprotectedvirtual
symex_assert(const goto_programt::instructiont &, statet &)goto_symextprotected
symex_assign(statet &state, const exprt &lhs, const exprt &rhs)goto_symextprotected
symex_assume(statet &state, const exprt &cond)goto_symextprotectedvirtual
symex_assume_l2(statet &, const exprt &cond)goto_symextprotected
symex_atomic_begin(statet &state)goto_symextprotectedvirtual
symex_atomic_end(statet &state)goto_symextprotectedvirtual
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_symextprotected
symex_configgoto_symextprotected
symex_coveragesymex_bmctprotected
symex_cpp_delete(statet &state, const codet &code)goto_symextprotectedvirtual
symex_cpp_new(statet &state, const exprt &lhs, const side_effect_exprt &code)goto_symextprotectedvirtual
symex_dead(statet &state)goto_symextprotectedvirtual
symex_dead(statet &state, const symbol_exprt &symbol_expr)goto_symextprotected
symex_decl(statet &state)goto_symextprotectedvirtual
symex_decl(statet &state, const symbol_exprt &expr)goto_symextprotectedvirtual
symex_end_of_function(statet &)goto_symextprotectedvirtual
symex_from_entry_point_of(const get_goto_functiont &get_goto_function, const shadow_memory_field_definitionst &fields)goto_symextvirtual
symex_function_call(const get_goto_functiont &get_goto_function, statet &state, const goto_programt::instructiont &instruction)goto_symextprotectedvirtual
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_symextprotectedvirtual
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_symextprotectedvirtual
symex_goto(statet &state)goto_symextprotectedvirtual
symex_input(statet &state, const codet &code)goto_symextprotectedvirtual
symex_other(statet &state)goto_symextprotectedvirtual
symex_output(statet &state, const codet &code)goto_symextprotectedvirtual
symex_printf(statet &state, const exprt &rhs)goto_symextprotectedvirtual
symex_set_return_value(statet &state, const exprt &return_value)goto_symextprotected
symex_start_thread(statet &state)goto_symextprotectedvirtual
symex_step(const get_goto_functiont &get_goto_function, statet &state) overridesymex_bmctprotectedvirtual
symex_threaded_step(statet &state, const get_goto_functiont &get_goto_function)goto_symextprotected
symex_throw(statet &state)goto_symextprotected
symex_unreachable_goto(statet &state)goto_symextprotected
symex_va_start(statet &, const exprt &lhs, const side_effect_exprt &)goto_symextprotectedvirtual
symex_with_state(statet &state, const get_goto_functiont &get_goto_functions)goto_symextvirtual
targetgoto_symextprotected
trigger_auto_object(const exprt &, statet &)goto_symextprotected
try_evaluate_constant(const statet &state, const exprt &expr)goto_symextprotectedstatic
try_evaluate_constant_string(const statet &state, const exprt &content)goto_symextprotected
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_symextprotected
unwindsetsymex_bmct
validate(const validation_modet vm) constgoto_symextinline
vcc(const exprt &cond, const irep_idt &property_id, const std::string &msg, statet &state)goto_symextprotectedvirtual
~goto_symext()=defaultgoto_symextvirtual