witness_provider.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Interface for outputting GraphML Witnesses for Goto Checkers
 
Author: Daniel Kroening, Peter Schrammel
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_CHECKER_WITNESS_PROVIDER_H
#define CPROVER_GOTO_CHECKER_WITNESS_PROVIDER_H
 
class goto_tracet;
 
class witness_providert
{
public:
  virtual ~witness_providert() = default;
 
  // Outputs an error witness in GraphML format (see `graphml_witnesst`)
  virtual void output_error_witness(const goto_tracet &) = 0;
 
  // Outputs a proof in GraphML format (see `graphml_witnesst`)
  virtual void output_proof() = 0;
};
class witness_providert {…};
 
#endif // CPROVER_GOTO_CHECKER_WITNESS_PROVIDER_H