grapht Class Reference

#include <witnesses.h>

Public Types
enum	typet { VIOLATION , CORRECTNESS }

Public Member Functions
	grapht (typettypet t)
void	generate_graphml (optionst &options, const std::string &output_path_override="")
	Generate the GraphML witness.
void	check_create_new_thread (BigInt thread_id, nodet *prev_node)

Public Attributes
typettypet	witness_type
std::string	verified_file
std::vector< edget >	edges

Member Enumeration Documentation

typet

enum grapht::typet

Enumerator
VIOLATION
CORRECTNESS

Constructor & Destructor Documentation

grapht()

grapht::grapht ( typettypet t )

inline

Member Function Documentation

check_create_new_thread()

void grapht::check_create_new_thread	(	BigInt	thread_id,
		nodet *	prev_node )

generate_graphml()

void grapht::generate_graphml	(	optionst &	options,
		const std::string &	output_path_override = "" )

Generate the GraphML witness.

The output path is taken from options["witness-output-graphml"] unless output_path_override is non-empty, in which case the override wins. Used by –all-witnesses to fan out per-witness filenames without mutating the global option (which would race under –parallel-solving).

Member Data Documentation

edges

std::vector<edget> grapht::edges

verified_file

std::string grapht::verified_file

witness_type

typettypet grapht::witness_type

---

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

• src/goto-symex/witness/witnesses.h
• src/goto-symex/witness/witnesses.cpp