witness_providert Class Reference

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

Implemented in single_path_symex_checkert, single_loop_incremental_symex_checkert, and multi_path_symex_checkert.

output_proof()

virtual void witness_providert::output_proof ( )

pure virtual

Implemented in single_path_symex_checkert, single_loop_incremental_symex_checkert, and multi_path_symex_checkert.

---

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

• /home/runner/work/cbmc/cbmc/src/goto-checker/witness_provider.h