12 #ifndef CPROVER_CBMC_SYMEX_BMC_H 13 #define CPROVER_CBMC_SYMEX_BMC_H 59 const std::string &path)
const 76 typedef std::unordered_map<irep_idt, unsigned, irep_id_hash>
loop_limitst;
100 const unsigned thread_nr,
110 #endif // CPROVER_CBMC_SYMEX_BMC_H
void set_unwind_loop_limit(const irep_idt &id, unsigned limit)
bool generate_report(const goto_functionst &goto_functions, const std::string &path) const
virtual bool get_unwind(const symex_targett::sourcet &source, unsigned unwind)
void set_unwind_limit(unsigned limit)
std::map< unsigned, loop_limitst > thread_loop_limitst
bool output_coverage_report(const goto_functionst &goto_functions, const std::string &path) const
symex_coveraget symex_coverage
virtual void merge_goto(const statet::goto_statet &goto_state, statet &state)
thread_loop_limitst thread_loop_limits
The main class for the forward symbolic simulator.
std::unordered_map< irep_idt, unsigned, irep_id_hash > loop_limitst
virtual bool get_unwind_recursion(const irep_idt &identifier, const unsigned thread_nr, unsigned unwind)
source_locationt last_source_location
Record and print code coverage of symbolic execution.
std::unordered_set< irep_idt, irep_id_hash > body_warnings
virtual void symex_step(const goto_functionst &goto_functions, statet &state)
show progress
symex_bmct(const namespacet &_ns, symbol_tablet &_new_symbol_table, symex_targett &_target)
void set_unwind_thread_loop_limit(unsigned thread_nr, const irep_idt &id, unsigned limit)
virtual void no_body(const irep_idt &identifier)