9#ifndef CPROVER_GOTO_CHECKER_SYMEX_BMC_INCREMENTAL_ONE_LOOP_H
10#define CPROVER_GOTO_CHECKER_SYMEX_BMC_INCREMENTAL_ONE_LOOP_H
41 std::unique_ptr<goto_symext::statet>
state;
49 unsigned unwind)
override;
const symbol_table_baset & outer_symbol_table
The symbol table associated with the goto-program being executed.
static get_goto_functiont get_goto_function(abstract_goto_modelt &goto_model)
Return a function to get/load a goto function from the given goto model Create a default delegate to ...
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
The type of delegate functions that retrieve a goto_functiont for a particular function identifier.
Storage for symbolic execution paths to be resumed later.
const unsigned incr_min_unwind
ui_message_handlert::uit output_ui
bool resume(const get_goto_functiont &get_goto_function)
Return true if symex can be resumed.
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)
bool from_entry_point_of(const get_goto_functiont &get_goto_function, symbol_tablet &new_symbol_table)
Return true if symex can be resumed.
const unsigned incr_max_unwind
const irep_idt incr_loop_id
void log_unwinding(unsigned unwind)
bool check_break(const irep_idt &loop_id, unsigned unwind) override
Defines condition for interrupting symbolic execution for incremental BMC.
std::unique_ptr< goto_symext::statet > state
bool should_stop_unwind(const symex_targett::sourcet &source, const call_stackt &context, unsigned unwind) override
Determine whether to unwind a loop.
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)
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
guard_expr_managert guard_managert
Identifies source in the context of symbolic execution.
Bounded Model Checking for ANSI-C.