goto_trace_provider.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Interface for returning Goto Traces from Goto Checkers
 
Author: Daniel Kroening, Peter Schrammel
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_CHECKER_GOTO_TRACE_PROVIDER_H
#define CPROVER_GOTO_CHECKER_GOTO_TRACE_PROVIDER_H
 
#include <util/irep.h>
 
class goto_tracet;
class namespacet;
 
class goto_trace_providert
{
public:
  virtual goto_tracet build_full_trace() const = 0;
 
  virtual goto_tracet build_shortest_trace() const = 0;
 
  virtual goto_tracet build_trace(const irep_idt &property_id) const = 0;
 
  virtual const namespacet &get_namespace() const = 0;
 
  virtual ~goto_trace_providert() = default;
};
class goto_trace_providert {…};
 
#endif // CPROVER_GOTO_CHECKER_GOTO_TRACE_PROVIDER_H