#include <goto-programs/goto_program.h>
#include <util/irep/location.h>
#include <atomic>
#include <cstddef>
#include <map>
#include <mutex>
#include <set>
#include <string>

Include dependency graph for property_verdict.h:

This graph shows which files directly or indirectly include this file:

Classes
struct	property_locationt
	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...
struct	property_resultt
	A verdict together with where it applies and a note explaining how it was reached – that a discharge came from interval analysis rather than the solver, or that it was vacuous. More...
class	property_verdict_tablet
	One verdict per property for a whole verification run. More...

Enumerations
enum class	property_verdictt { NotChecked = 0 , Passed = 1 , Unknown = 2 , Failed = 3 }
	Outcome of checking one property. More...

Functions
property_locationt	property_location (const goto_programt::instructiont &pc, const std::string &description)
	Where the claim `description` raised at `pc` lives, with the assertion's instruction and condition when the claim is `pc's` own assertion.
std::string	property_key (const goto_programt::instructiont &pc, const std::string &description)
	The table key for the claim `description` raised at `pc`.
bool	withholds_proofs (const optionst &options)
	Whether a phase must leave a claim it discharges NotChecked rather than Passed: under a k-step strategy, a base case always, and any other phase while its round is incomplete.

Enumeration Type Documentation

◆ property_verdictt

enum class property_verdictt

strong

Outcome of checking one property.

Ordered by dominance: when a property is checked more than once in a run, the numerically greater verdict survives.

NotChecked is the weakest so that seeding the table with the program's whole property set never masks a real verdict recorded later. It is not a failure to report it: without –multi-property ESBMC solves one monolithic formula and stops at the first violation, so the properties it never separated out have genuinely not been decided, and saying so beats claiming they passed.

Enumerator
NotChecked
Passed
Unknown
Failed

Function Documentation

◆ property_key()

std::string property_key	(	const goto_programt::instructiont &	pc,
		const std::string &	description )

The table key for the claim description raised at pc.

Two assertions can share a description and a source position – a[i] + a[j] has two array bound checks on one column – so an assertion's key also names its instruction; without it they share a row, and one's violation skips the other. Any other claim symex raises there, such as a dereference check in the asserted expression, keeps description and position only.

◆ property_location()

property_locationt property_location	(	const goto_programt::instructiont &	pc,
		const std::string &	description )

Where the claim description raised at pc lives, with the assertion's instruction and condition when the claim is pc's own assertion.

◆ withholds_proofs()

bool withholds_proofs ( const optionst & options )

Whether a phase must leave a claim it discharges NotChecked rather than Passed: under a k-step strategy, a base case always, and any other phase while its round is incomplete.

Classes