verification_result.h File Reference

Interface for the various verification engines providing results. More...

#include <map>
#include <memory>
#include <string>
#include <vector>

Include dependency graph for verification_result.h:

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

Go to the source code of this file.

Classes
struct	verification_resultt

Typedefs
typedef dstringt	irep_idt
using	propertiest = std::map< irep_idt, property_infot >

Enumerations
enum class	prop_statust {   NOT_CHECKED , UNKNOWN , NOT_REACHABLE , PASS ,   FAIL , ERROR }
enum class	verifier_resultt { UNKNOWN , PASS , FAIL , ERROR }

Functions
int	verifier_result_to_exit_code (verifier_resultt result)

Detailed Description

Interface for the various verification engines providing results.

Definition in file verification_result.h.

Typedef Documentation

irep_idt

typedef dstringt irep_idt

Definition at line 16 of file verification_result.h.

propertiest

using propertiest = std::map<irep_idt, property_infot>

Definition at line 19 of file verification_result.h.

Enumeration Type Documentation

prop_statust

enum prop_statust

strong

Enumerator
NOT_CHECKED	The property was not checked (also used for initialization)
UNKNOWN	The checker was unable to determine the status of the property.
NOT_REACHABLE	The property was proven to be unreachable.
PASS	The property was not violated.
FAIL	The property was violated.
ERROR	An error occurred during goto checking.

Definition at line 27 of file verification_result.h.

verifier_resultt

enum verifier_resultt

strong

Enumerator
UNKNOWN
PASS	No properties were violated.
FAIL	Some properties were violated.
ERROR	An error occurred during goto checking.

Definition at line 43 of file verification_result.h.

Function Documentation

verifier_result_to_exit_code()

int verifier_result_to_exit_code

(

verifier_resultt

result

)

Definition at line 155 of file verification_result.cpp.