12 #ifndef CPROVER_CBMC_SYMEX_BMC_H 13 #define CPROVER_CBMC_SYMEX_BMC_H 55 typedef std::function<
tvt(
const irep_idt &,
unsigned,
unsigned &)>
78 const std::string &path)
const 104 unsigned unwind)
override;
108 const unsigned thread_nr,
109 unsigned unwind)
override;
118 #endif // CPROVER_CBMC_SYMEX_BMC_H std::unordered_set< irep_idt > body_warnings
bool generate_report(const goto_functionst &goto_functions, const std::string &path) const
std::vector< recursion_unwind_handlert > recursion_unwind_handlers
Callbacks that may provide an unwind/do-not-unwind decision for a recursive call.
bool get_unwind_recursion(const irep_idt &identifier, const unsigned thread_nr, unsigned unwind) override
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
const bool record_coverage
void add_loop_unwind_handler(loop_unwind_handlert handler)
Add a callback function that will be called to determine whether to unwind loops.
void merge_goto(const statet::goto_statet &goto_state, statet &state) override
void add_recursion_unwind_handler(recursion_unwind_handlert handler)
Add a callback function that will be called to determine whether to unwind recursion.
Identifies source in the context of symbolic execution.
bool output_coverage_report(const goto_functionst &goto_functions, const std::string &path) const
symex_coveraget symex_coverage
const symbol_tablet & outer_symbol_table
The symbol table associated with the goto-program that we're executing.
A collection of goto functions.
path_storaget & path_storage
std::function< tvt(const goto_symex_statet::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 ...
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.
The main class for the forward symbolic simulator.
std::vector< framet > call_stackt
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 goto_symex_statet::call_stackt &context, unsigned unwind) override
symex_bmct(message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage)
void no_body(const irep_idt &identifier) override
source_locationt last_source_location
Record and print code coverage of symbolic execution.
std::vector< loop_unwind_handlert > loop_unwind_handlers
Callbacks that may provide an unwind/do-not-unwind decision for a loop.
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...
Storage of symbolic execution paths to resume.