yamlt Class Reference

#include <witnesses.h>

Public Types
enum	typet { VIOLATION , CORRECTNESS }

Public Member Functions
	yamlt (typettypet t)
void	generate_yaml (optionst &options, const std::string &output_path_override="")
	Generate the YAML witness.

Public Attributes
typettypet	witness_type
std::string	verified_file
std::vector< waypoint >	segments
std::vector< invariant >	invariants

Member Enumeration Documentation

typet

enum yamlt::typet

Enumerator
VIOLATION
CORRECTNESS

Constructor & Destructor Documentation

yamlt()

yamlt::yamlt ( typettypet t )

inline

Member Function Documentation

generate_yaml()

void yamlt::generate_yaml	(	optionst &	options,
		const std::string &	output_path_override = "" )

Generate the YAML witness.

The output path is taken from options["witness-output-yaml"] unless output_path_override is non-empty.

Member Data Documentation

invariants

std::vector<invariant> yamlt::invariants

segments

std::vector<waypoint> yamlt::segments

verified_file

std::string yamlt::verified_file

witness_type

typettypet yamlt::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