Where a property lives, kept apart from the table key so the report can sort by source position and print a path once per file rather than once per line. More...

#include <property_verdict.h>

Public Attributes
std::string	file
std::string	function
std::string	description
unsigned	line = 0
unsigned	column = 0
unsigned	instruction = 0
	The asserting instruction's location_number and condition, when the property is that instruction's own assertion: they order and label rows of assertions that share a description and a position.
expr2tc	condition

Detailed Description

Where a property lives, kept apart from the table key so the report can sort by source position and print a path once per file rather than once per line.

Member Data Documentation

◆ column

unsigned property_locationt::column = 0

◆ condition

expr2tc property_locationt::condition

◆ description

std::string property_locationt::description

◆ file

std::string property_locationt::file

◆ function

std::string property_locationt::function

◆ instruction

unsigned property_locationt::instruction = 0

The asserting instruction's location_number and condition, when the property is that instruction's own assertion: they order and label rows of assertions that share a description and a position.

◆ line

unsigned property_locationt::line = 0

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

src/goto-programs/property_verdict.h

Public Attributes