graphml_witnesst Class Reference

#include <graphml_witness.h>

Collaboration diagram for graphml_witnesst:

Public Member Functions
	graphml_witnesst (const namespacet &_ns)
void	operator() (const goto_tracet &goto_trace)
	counterexample witness More...
void	operator() (const symex_target_equationt &equation)
	proof witness More...
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)

Protected Attributes
const namespacet &	ns
graphmlt	graphml

Detailed Description

Definition at line 21 of file graphml_witness.h.

Constructor & Destructor Documentation

graphml_witnesst()

graphml_witnesst::graphml_witnesst ( const namespacet &  _ns )

inlineexplicit

Definition at line 24 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 51 of file graphml_witness.cpp.

graph()

const graphmlt& graphml_witnesst::graph ( )

inline

Definition at line 32 of file graphml_witness.h.

operator()() [1/2]

void graphml_witnesst::operator()

(

const goto_tracet &

goto_trace

)

counterexample witness

Definition at line 179 of file graphml_witness.cpp.

operator()() [2/2]

void graphml_witnesst::operator()

(

const symex_target_equationt &

equation

)

proof witness

Definition at line 356 of file graphml_witness.cpp.

remove_l0_l1()

void graphml_witnesst::remove_l0_l1 ( exprt &  expr )

protected

Definition at line 25 of file graphml_witness.cpp.

Member Data Documentation

graphml

graphmlt graphml_witnesst::graphml

protected

Definition at line 39 of file graphml_witness.h.

ns

const namespacet& graphml_witnesst::ns

protected

Definition at line 38 of file graphml_witness.h.

---

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

• goto-programs/graphml_witness.h
• goto-programs/graphml_witness.cpp