symex_bmc.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Bounded Model Checking for ANSI-C
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_CHECKER_SYMEX_BMC_H
#define CPROVER_GOTO_CHECKER_SYMEX_BMC_H
 
#include <util/threeval.h>
 
#include <goto-symex/goto_symex.h>
 
#include "symex_coverage.h"
 
class unwindsett;
 
class symex_bmct : public goto_symext
{
public:
  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);
 
  // To show progress
  source_locationt last_source_location;
 
  typedef std::function<
    tvt(const call_stackt &, unsigned, unsigned, unsigned &)>
    loop_unwind_handlert;
 
  typedef std::function<tvt(const irep_idt &, unsigned, unsigned &)>
    recursion_unwind_handlert;
 
  void add_loop_unwind_handler(loop_unwind_handlert handler)
  {
    loop_unwind_handlers.push_back(handler);
  }
 
  void add_recursion_unwind_handler(recursion_unwind_handlert handler)
  {
    recursion_unwind_handlers.push_back(handler);
  }
 
  bool output_coverage_report(
    const goto_functionst &goto_functions,
    const std::string &path) const
  {
    return symex_coverage.generate_report(goto_functions, path);
  }
 
  const bool record_coverage;
 
  unwindsett &unwindset;
 
protected:
  std::vector<loop_unwind_handlert> loop_unwind_handlers;
 
  std::vector<recursion_unwind_handlert> recursion_unwind_handlers;
 
  void symex_step(const get_goto_functiont &get_goto_function, statet &state)
    override;
 
  void merge_goto(
    const symex_targett::sourcet &source,
    goto_statet &&goto_state,
    statet &state) override;
 
  bool should_stop_unwind(
    const symex_targett::sourcet &source,
    const call_stackt &context,
    unsigned unwind) override;
 
  bool get_unwind_recursion(
    const irep_idt &identifier,
    unsigned thread_nr,
    unsigned unwind) override;
 
  symex_coveraget symex_coverage;
};
 
#endif // CPROVER_GOTO_CHECKER_SYMEX_BMC_H