Go to the documentation of this file.
9 #ifndef CPROVER_GOTO_CHECKER_SYMEX_BMC_INCREMENTAL_ONE_LOOP_H
10 #define CPROVER_GOTO_CHECKER_SYMEX_BMC_INCREMENTAL_ONE_LOOP_H
38 std::unique_ptr<goto_symext::statet>
state;
46 unsigned unwind)
override;
49 #endif // CPROVER_GOTO_CHECKER_SYMEX_BMC_INCREMENTAL_ONE_LOOP_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Storage for symbolic execution paths to be resumed later.
bool check_break(const irep_idt &loop_id, unsigned unwind) override
Defines condition for interrupting symbolic execution for incremental BMC.
This is unused by this implementation of guards, but can be used by other implementations of the same...
const symbol_tablet & outer_symbol_table
The symbol table associated with the goto-program being executed.
std::unique_ptr< goto_symext::statet > state
const unsigned incr_max_unwind
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
bool should_stop_unwind(const symex_targett::sourcet &source, const call_stackt &context, unsigned unwind) override
Determine whether to unwind a loop.
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 ...
const unsigned incr_min_unwind
const irep_idt incr_loop_id
bool resume(const get_goto_functiont &get_goto_function)
Return true if symex can be resumed.
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.
Identifies source in the context of symbolic execution.
symex_bmc_incremental_one_loopt(message_handlert &, const symbol_tablet &outer_symbol_table, symex_target_equationt &, const optionst &, path_storaget &, guard_managert &)
bool from_entry_point_of(const get_goto_functiont &get_goto_function, symbol_tablet &new_symbol_table)
Return true if symex can be resumed.