Loading...

Searching...

No Matches

Classes | Enumerations | Functions

static_verifier.h File Reference

#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:

[フレーム]

Go to the source code of 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.