graphml_witnesst Class Reference

#include <graphml_witness.h>

Collaboration diagram for graphml_witnesst:

Classes
struct	pair_hash

Public Member Functions
	graphml_witnesst (const namespacet &_ns)
void	operator() (const goto_tracet &goto_trace)
	counterexample witness
void	operator() (const symex_target_equationt &equation)
	proof witness
const graphmlt &	graph ()

Protected Member Functions
void	remove_l0_l1 (exprt &expr)
std::string	convert_assign_rec (const irep_idt &identifier, const code_assignt &assign)

Static Protected Member Functions
template<typename T >
static void	hash_combine (std::size_t &seed, const T &v)

Protected Attributes
const namespacet &	ns
graphmlt	graphml
std::unordered_map< std::pair< unsigned int, const irept::dt * >, std::string, pair_hash< unsigned int, const irept::dt * > >	cache

Detailed Description

Definition at line 23 of file graphml_witness.h.

Constructor & Destructor Documentation

graphml_witnesst()

graphml_witnesst::graphml_witnesst ( const namespacet &  _ns )

inlineexplicit

Definition at line 26 of file graphml_witness.h.

Member Function Documentation

convert_assign_rec()

std::string graphml_witnesst::convert_assign_rec ( const irep_idt &  identifier, const code_assignt &  assign  )

protected

Definition at line 74 of file graphml_witness.cpp.

graph()

const graphmlt & graphml_witnesst::graph ( )

inline

Definition at line 34 of file graphml_witness.h.

hash_combine()

template<typename T >

static void graphml_witnesst::hash_combine ( std::size_t &  seed, const T &  v  )

inlinestaticprotected

Definition at line 49 of file graphml_witness.h.

operator()() [1/2]

void graphml_witnesst::operator()

(

const goto_tracet &

goto_trace

)

counterexample witness

Definition at line 278 of file graphml_witness.cpp.

operator()() [2/2]

void graphml_witnesst::operator()

(

const symex_target_equationt &

equation

)

proof witness

Definition at line 524 of file graphml_witness.cpp.

remove_l0_l1()

void graphml_witnesst::remove_l0_l1 ( exprt &  expr )

protected

Definition at line 42 of file graphml_witness.cpp.

Member Data Documentation

cache

std::unordered_map< std::pair<unsigned int, const irept::dt *>, std::string, pair_hash<unsigned int, const irept::dt *> > graphml_witnesst::cache

protected

Definition at line 70 of file graphml_witness.h.

graphml

graphmlt graphml_witnesst::graphml

protected

Definition at line 41 of file graphml_witness.h.

ns

const namespacet& graphml_witnesst::ns

protected

Definition at line 40 of file graphml_witness.h.

---

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

• /home/runner/work/cbmc/cbmc/src/goto-programs/graphml_witness.h
• /home/runner/work/cbmc/cbmc/src/goto-programs/graphml_witness.cpp