invariant Class Reference

#include <witnesses.h>

Public Types
enum	Type {   loop_invariant , loop_transition_invariant , location_invariant , location_transition_invariant ,   unknown }

Public Attributes
Type	type = unknown
std::string	file
std::string	value
std::string	format
BigInt	line = c_nonset
BigInt	column = c_nonset
std::string	function

Member Enumeration Documentation

Type

enum invariant::Type

Enumerator
loop_invariant
loop_transition_invariant
location_invariant
location_transition_invariant
unknown

Member Data Documentation

column

BigInt invariant::column = c_nonset

file

std::string invariant::file

format

std::string invariant::format

function

std::string invariant::function

line

BigInt invariant::line = c_nonset

type

Type invariant::type = unknown

value

std::string invariant::value

---

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

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