multi_path_symex_checker.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Goto Checker using Multi-Path Symbolic Execution
 
Author: Daniel Kroening, Peter Schrammel
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_CHECKER_H
#define CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_CHECKER_H
 
#include "fault_localization_provider.h"
#include "goto_symex_property_decider.h"
#include "goto_trace_provider.h"
#include "multi_path_symex_only_checker.h"
#include "witness_provider.h"
 
#include <chrono> // IWYU pragma: keep
 
class multi_path_symex_checkert : public multi_path_symex_only_checkert,
                                  public goto_trace_providert,
                                  public witness_providert,
                                  public fault_localization_providert
{
public:
  multi_path_symex_checkert(
    const optionst &options,
    ui_message_handlert &ui_message_handler,
    abstract_goto_modelt &goto_model);
 
  resultt operator()(propertiest &) override;
 
  goto_tracet build_full_trace() const override;
  goto_tracet build_shortest_trace() const override;
  goto_tracet build_trace(const irep_idt &) const override;
  const namespacet &get_namespace() const override;
 
  void output_error_witness(const goto_tracet &) override;
  void output_proof() override;
 
  fault_location_infot
  localize_fault(const irep_idt &property_id) const override;
 
  void report() override;
 
protected:
  bool equation_generated;
  goto_symex_property_decidert property_decider;
 
  virtual std::chrono::duration<double>
  prepare_property_decider(propertiest &properties);
 
  virtual void run_property_decider(
    incremental_goto_checkert::resultt &result,
    propertiest &properties,
    std::chrono::duration<double> solver_runtime);
};
 
#endif // CPROVER_GOTO_CHECKER_MULTI_PATH_SYMEX_CHECKER_H