CBMC
witness_providert Class Referenceabstract

An implementation of incremental_goto_checkert may implement this interface to provide GraphML witnesses. More...

#include <witness_provider.h>

+ Inheritance diagram for witness_providert:

Public Member Functions

virtual ~witness_providert ()=default
 
virtual void output_error_witness (const goto_tracet &)=0
 
virtual void output_proof ()=0
 

Detailed Description

An implementation of incremental_goto_checkert may implement this interface to provide GraphML witnesses.

Definition at line 19 of file witness_provider.h.

Constructor & Destructor Documentation

◆ ~witness_providert()

virtual witness_providert::~witness_providert ( )
virtualdefault

Member Function Documentation

◆ output_error_witness()

virtual void witness_providert::output_error_witness ( const goto_tracet )
pure virtual

◆ output_proof()

virtual void witness_providert::output_proof ( )
pure virtual

The documentation for this class was generated from the following file: