CBMC
Classes | Public Member Functions | Protected Member Functions | Static Protected Member Functions | Protected Attributes | List of all members
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 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)
 

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 280 of file graphml_witness.cpp.

◆ operator()() [2/2]

void graphml_witnesst::operator() ( const symex_target_equationt &  equation)

proof witness

Definition at line 526 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: