#include <goto-checker/properties.h>
#include <iosfwd>
#include <analyses/ai_history.h>

Include dependency graph for static_verifier.h:

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

Classes
class	static_verifier_resultt
	The result of verifying a single assertion As well as the status of the assertion (see above), it also contains the location (source_location and function_id) and the set of histories in which the assertion is unknown or false, so that more detailed post-processing or error output can be done. More...

Enumerations
enum class	ai_verifier_statust { TRUE , FALSE_IF_REACHABLE , NOT_REACHABLE , UNKNOWN }
	An ai_baset contains zero or more histories that reach a location. More...

Functions
bool	static_verifier (const goto_modelt &, const ai_baset &, const optionst &, message_handlert &, std::ostream &)
	Runs the analyzer and then prints out the domain.
void	static_verifier (const abstract_goto_modelt &abstract_goto_model, const ai_baset &ai, propertiest &properties)
	Use the information from the abstract interpreter to fill out the statuses of the passed properties.
std::string	as_string (const ai_verifier_statust &)
	Makes a status message string from a status.

Enumeration Type Documentation

◆ ai_verifier_statust

enum class ai_verifier_statust

strong

An ai_baset contains zero or more histories that reach a location.

In a given history, a Boolean expression can be true, false or unknown. If we only care about "does there exist a history that make the condition true/false/unknown" then that means there are 8 possible statuses. In practice not all of them are usefully distinguishable, so we only consider 4 of them. Also note that because abstract interpretation is an over-approximate analysis, the existence of a history does not necessarily mean that there is an actual executation trace that makes the condition true/false.

Enumerator
TRUE
FALSE_IF_REACHABLE
NOT_REACHABLE
UNKNOWN

Definition at line 51 of file static_verifier.h.

Function Documentation

◆ as_string()

std::string as_string ( const ai_verifier_statust & status )

Makes a status message string from a status.

Definition at line 23 of file static_verifier.cpp.

◆ static_verifier() [1/2]

void static_verifier	(	const abstract_goto_modelt &	abstract_goto_model,
		const ai_baset &	ai,
		propertiest &	properties )

Use the information from the abstract interpreter to fill out the statuses of the passed properties.

Parameters

abstract_goto_model	The goto program to verify
ai	The abstract interpreter (should be run to fixpoint before calling this function)
properties	The properties to fill out

Definition at line 229 of file static_verifier.cpp.

◆ static_verifier() [2/2]

bool static_verifier	(	const goto_modelt &	goto_model,
		const ai_baset &	ai,
		const optionst &	options,
		message_handlert &	message_handler,
		std::ostream &	out )

Runs the analyzer and then prints out the domain.

Parameters

goto_model	the program analyzed
ai	the abstract interpreter after it has been run to fix point
options	the parsed user options
message_handler	the system message handler
out	output stream for the printing

Returns: false on success with the domain printed to out

Definition at line 403 of file static_verifier.cpp.

Classes