#include <goto-programs/goto_functions.h>
#include <goto-programs/property_verdict.h>
#include <util/config/options.h>
#include <cstdint>
#include <cstdlib>

Include dependency graph for property_verdict.cpp:

Functions
static property_locationt	property_location (const locationt &location, const std::string &description)
static bool	is_own_assertion (const goto_programt::instructiont &pc, const std::string &desc)
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.

Function Documentation

◆ is_own_assertion()

bool is_own_assertion	(	const goto_programt::instructiont &	pc,
		const std::string &	desc )

static

◆ 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() [1/2]

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.

◆ property_location() [2/2]

property_locationt property_location	(	const locationt &	location,
		const std::string &	description )

static

◆ 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.