12#ifndef CPROVER_GOTO_CHECKER_SYMEX_BMC_H
13#define CPROVER_GOTO_CHECKER_SYMEX_BMC_H
44 typedef std::function<
54 typedef std::function<
tvt(
const irep_idt &,
unsigned,
unsigned &)>
77 const std::string &path)
const
105 unsigned unwind)
override;
110 unsigned unwind)
override;
A collection of goto functions.
Container for data that varies per program point, e.g.
goto_symex_statet statet
A type abbreviation for goto_symex_statet.
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 ...
guard_managert & guard_manager
Used to create guards.
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)
Construct a goto_symext to execute a particular program.
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.
symex_coveraget symex_coverage
bool get_unwind_recursion(const irep_idt &identifier, unsigned thread_nr, unsigned unwind) override
std::vector< loop_unwind_handlert > loop_unwind_handlers
Callbacks that may provide an unwind/do-not-unwind decision for a loop.
void merge_goto(const symex_targett::sourcet &source, goto_statet &&goto_state, statet &state) override
Merge a single branch, the symbolic state of which is held in goto_state, into the current overall sy...
std::function< tvt(const call_stackt &, unsigned, unsigned, unsigned &)> loop_unwind_handlert
Loop unwind handlers take the call stack, loop number, the unwind count so far, and an out-parameter ...
source_locationt last_source_location
bool output_coverage_report(const goto_functionst &goto_functions, const std::string &path) const
void add_recursion_unwind_handler(recursion_unwind_handlert handler)
Add a callback function that will be called to determine whether to unwind recursion.
std::vector< recursion_unwind_handlert > recursion_unwind_handlers
Callbacks that may provide an unwind/do-not-unwind decision for a recursive call.
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)
void symex_step(const get_goto_functiont &get_goto_function, statet &state) override
show progress
bool should_stop_unwind(const symex_targett::sourcet &source, const call_stackt &context, unsigned unwind) override
Determine whether to unwind a loop.
void add_loop_unwind_handler(loop_unwind_handlert handler)
Add a callback function that will be called to determine whether to unwind loops.
const bool record_coverage
std::function< tvt(const irep_idt &, unsigned, unsigned &)> recursion_unwind_handlert
Recursion unwind handlers take the function ID, the unwind count so far, and an out-parameter specify...
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.
Record and print code coverage of symbolic execution.