property_verdict_tablet Class Reference

One verdict per property for a whole verification run. More...

#include <property_verdict.h>

Public Member Functions
void	record (const std::string &property, property_verdictt verdict, const property_locationt &loc, const std::string &note="")
	Records verdict for property at loc, annotated with note.
void	promote_unchecked_to_passed ()
	Raises every NotChecked entry recorded since the last begin_round() or clear() to Passed.
void	note_incomplete ()
	Records that a phase stopped before every property reached a verdict, disarming proofs until the next round completes.
void	begin_round ()
	Starts the round of a k-step strategy's next base case, incomplete until complete_round().
void	complete_round ()
	Records that the round's base case solved every claim it raised.
bool	is_incomplete () const
	Whether a phase since the last clear() or complete_round() stopped short, or the round's base case has not completed.
bool	all_passed () const
	Whether every property in the table reached Passed.
std::size_t	size () const
	How many distinct properties have been checked.
bool	has_violation () const
	Whether any property has been found violated.
std::map< std::string, property_resultt >	snapshot () const
	A copy of the results recorded so far, keyed by property.
void	clear ()
	Discards all verdicts.

Detailed Description

One verdict per property for a whole verification run.

--multi-property re-checks every property in every thread interleaving, and a property can be discharged under one schedule while being violated under another. Reporting each check as it happens then prints contradictory verdicts for a single source assertion (esbmc/esbmc discussion #6391). Recording verdicts here instead lets the run report each property once, with the dominant verdict.

Member Function Documentation

all_passed()

bool property_verdict_tablet::all_passed

(

)

const

Whether every property in the table reached Passed.

A k-step run's verdict follows its table (§4 of docs/roadmap/multi-property-strategy-plan.md), so a row it could not settle, or settled only vacuously, is not a proof of the program.

begin_round()

void property_verdict_tablet::begin_round

(

)

Starts the round of a k-step strategy's next base case, incomplete until complete_round().

A row this round never records is not promoted.

clear()

void property_verdict_tablet::clear

(

)

Discards all verdicts.

complete_round()

void property_verdict_tablet::complete_round ( )

inline

Records that the round's base case solved every claim it raised.

has_violation()

bool property_verdict_tablet::has_violation ( ) const

inline

Whether any property has been found violated.

Lock-free, so it stays usable from the SIGALRM timeout handler, which must report an already-established violation before _exit() discards it.

is_incomplete()

bool property_verdict_tablet::is_incomplete ( ) const

inline

Whether a phase since the last clear() or complete_round() stopped short, or the round's base case has not completed.

note_incomplete()

void property_verdict_tablet::note_incomplete

(

)

Records that a phase stopped before every property reached a verdict, disarming proofs until the next round completes.

promote_unchecked_to_passed()

void property_verdict_tablet::promote_unchecked_to_passed

(

)

Raises every NotChecked entry recorded since the last begin_round() or clear() to Passed.

Call only once the run has established that all properties hold – a monolithic UNSAT refutes the disjunction of every claim violation, so each claim holds – and never after a merely bounded round such as a k-induction base case. Does nothing while is_incomplete().

record()

void property_verdict_tablet::record	(	const std::string &	property,
		property_verdictt	verdict,
		const property_locationt &	loc,
		const std::string &	note = "" )

Records verdict for property at loc, annotated with note.

Keeps the dominant verdict when the property has already been checked. Safe to call from parallel solver threads.

loc is required rather than defaulted: the report sorts and groups on it, so a caller that does not know where its property is would silently sort to the top of the table with no file or line.

size()

std::size_t property_verdict_tablet::size

(

)

const

How many distinct properties have been checked.

snapshot()

std::map< std::string, property_resultt > property_verdict_tablet::snapshot

(

)

const

A copy of the results recorded so far, keyed by property.

---

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

• src/goto-programs/property_verdict.h
• src/goto-programs/property_verdict.cpp