Properties. More...

#include <map>
#include <goto-programs/goto_program.h>

Include dependency graph for properties.h:

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

Classes
struct	property_infot

Typedefs
typedef std::map< irep_idt, property_infot >	propertiest
	A map of property IDs to property infos. More...

Enumerations
enum class	property_statust { NOT_CHECKED , UNKNOWN , NOT_REACHABLE , PASS , FAIL , ERROR }
	The status of a property. More...

enum class	resultt { UNKNOWN , PASS , FAIL , ERROR }
	The result of goto verifying. More...

Functions
std::string	as_string (property_statust)

std::string	as_string (resultt)

propertiest	initialize_properties (const abstract_goto_modelt &)
	Returns the properties in the goto model. More...

void	update_properties_from_goto_model (propertiest &properties, const abstract_goto_modelt &goto_model)
	Updates `properties` with the assertions in `goto_model`. More...

std::string	as_string (const irep_idt &property_id, const property_infot &property_info)

xmlt	xml (const irep_idt &property_id, const property_infot &property_info)

json_objectt	json (const irep_idt &property_id, const property_infot &property_info)

void	json (json_stream_objectt &, const irep_idt &, const property_infot &)
	Write the property info into the given JSON stream object. More...

int	result_to_exit_code (resultt result)

std::size_t	count_properties (const propertiest &, property_statust)
	Return the number of properties with given `status`. More...

bool	is_property_to_check (property_statust)
	Return true if the status is NOT_CHECKED or UNKNOWN. More...

bool	has_properties_to_check (const propertiest &properties)
	Return true if there as a property with NOT_CHECKED or UNKNOWN status. More...

property_statust &	operator\|= (property_statust &, property_statust const &)
	Update with the preference order. More...

property_statust &	operator&= (property_statust &, property_statust const &)
	Update with the preference order. More...

resultt	determine_result (const propertiest &properties)
	Determines the overall result corresponding from the given properties That is PASS if all properties are PASS or NOT_CHECKED, FAIL if at least one property is FAIL and no property is ERROR, UNKNOWN if no property is FAIL or ERROR and at least one property is UNKNOWN, ERROR if at least one property is error. More...

Detailed Description

Properties.

Definition in file properties.h.

Typedef Documentation

◆ propertiest

typedef std::map<irep_idt, property_infot> propertiest

A map of property IDs to property infos.

Definition at line 76 of file properties.h.

Enumeration Type Documentation

◆ property_statust

enum property_statust

strong

The status of a property.

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 25 of file properties.h.

◆ resultt

enum resultt

strong

The result of goto verifying.

Enumerator
UNKNOWN	No property was violated, neither was there an error.
PASS	No properties were violated.
FAIL	Some properties were violated.
ERROR	An error occurred during goto checking.

Definition at line 44 of file properties.h.

Function Documentation

◆ as_string() [1/3]

std::string as_string	(	const irep_idt &	property_id,
		const property_infot &	property_info
	)

Definition at line 104 of file properties.cpp.

◆ as_string() [2/3]

std::string as_string ( property_statust status )

Definition at line 41 of file properties.cpp.

◆ as_string() [3/3]

std::string as_string ( resultt result )

Definition at line 24 of file properties.cpp.

◆ count_properties()

std::size_t count_properties	(	const propertiest &	properties,
		property_statust	status
	)

Return the number of properties with given status.

Definition at line 164 of file properties.cpp.

◆ determine_result()

resultt determine_result ( const propertiest & properties )

Determines the overall result corresponding from the given properties That is PASS if all properties are PASS or NOT_CHECKED, FAIL if at least one property is FAIL and no property is ERROR, UNKNOWN if no property is FAIL or ERROR and at least one property is UNKNOWN, ERROR if at least one property is error.

Definition at line 264 of file properties.cpp.

◆ has_properties_to_check()

bool has_properties_to_check ( const propertiest & properties )

Return true if there as a property with NOT_CHECKED or UNKNOWN status.

Definition at line 181 of file properties.cpp.

◆ initialize_properties()

propertiest initialize_properties ( const abstract_goto_modelt & goto_model )

Returns the properties in the goto model.

Definition at line 70 of file properties.cpp.

◆ is_property_to_check()

bool is_property_to_check ( property_statust status )

Return true if the status is NOT_CHECKED or UNKNOWN.

Definition at line 175 of file properties.cpp.

◆ json() [1/2]

json_objectt json	(	const irep_idt &	property_id,
		const property_infot &	property_info
	)

Definition at line 132 of file properties.cpp.

◆ json() [2/2]

void json	(	json_stream_objectt &	result,
		const irep_idt &	property_id,
		const property_infot &	property_info
	)

Write the property info into the given JSON stream object.

Definition at line 139 of file properties.cpp.

◆ operator&=()

property_statust& operator&=	(	property_statust &	a,
		property_statust const &	b
	)

Update with the preference order.

ERROR
FAIL
UNKNOWN
NOT_CHECKED
NOT_REACHABLE
PASS Suitable for computing overall results

Definition at line 231 of file properties.cpp.

◆ operator|=()

property_statust& operator\|=	(	property_statust &	a,
		property_statust const &	b
	)

Update with the preference order.

old non-UNKNOWN/non-NOT_CHECKED status
new non-UNKNOWN/non-NOT_CHECKED status
UNKNOWN
NOT_CHECKED Suitable for updating property status

Definition at line 197 of file properties.cpp.

◆ result_to_exit_code()

int result_to_exit_code ( resultt result )

Definition at line 147 of file properties.cpp.

◆ update_properties_from_goto_model()

void update_properties_from_goto_model	(	propertiest &	properties,
		const abstract_goto_modelt &	goto_model
	)

Updates properties with the assertions in goto_model.

Definition at line 77 of file properties.cpp.

◆ xml()

xmlt xml	(	const irep_idt &	property_id,
		const property_infot &	property_info
	)

Definition at line 110 of file properties.cpp.

Classes

Typedefs

Enumerations

Functions