properties.cpp File Reference

Properties. More...

#include "properties.h"
#include <util/exit_codes.h>
#include <util/invariant.h>
#include <util/json.h>
#include <util/json_irep.h>
#include <util/json_stream.h>
#include <util/xml.h>
#include <util/xml_irep.h>
#include <goto-programs/abstract_goto_model.h>

Include dependency graph for properties.cpp:

Go to the source code of this file.

Functions
std::string	as_string (resultt result)
std::string	as_string (property_statust status)
propertiest	initialize_properties (const abstract_goto_modelt &goto_model)
	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)
template<class json_objectT >
static void	json (json_objectT &result, 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 &result, const irep_idt &property_id, const property_infot &property_info)
	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 &properties, property_statust status)
	Return the number of properties with given status. More...
bool	is_property_to_check (property_statust status)
	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 &a, property_statust const &b)
	Update with the preference order. More...
property_statust &	operator&= (property_statust &a, property_statust const &b)
	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.cpp.

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/3]

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

Definition at line 132 of file properties.cpp.

json() [2/3]

template<class json_objectT >

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

static

Definition at line 120 of file properties.cpp.

json() [3/3]

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.

1. ERROR
2. FAIL
3. UNKNOWN
4. NOT_CHECKED
5. NOT_REACHABLE
6. 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.

1. old non-UNKNOWN/non-NOT_CHECKED status
2. new non-UNKNOWN/non-NOT_CHECKED status
3. UNKNOWN
4. 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.