Loading...

Searching...

No Matches

graphml_witnesst Class Reference

#include <graphml_witness.h>

+ Collaboration diagram for graphml_witnesst:

[フレーム]

[legend]

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

◆ operator()() [2/2]

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

proof witness

Definition at line 584 of file graphml_witness.cpp.

◆ remove_l0_l1()

void graphml_witnesst::remove_l0_l1 ( exprt & expr )

protected

Definition at line 43 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