CBMC
Loading...
Searching...
No Matches
Classes | Typedefs | Enumerations | Functions
properties.h File Reference

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:

Go to the source code of this file.

Classes

struct   property_infot
 

Typedefs

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

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.
 
void  update_properties_from_goto_model (propertiest &properties, const abstract_goto_modelt &goto_model)
  Updates properties with the assertions in goto_model.
 
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.
 
int  result_to_exit_code (resultt result)
 
std::size_t  count_properties (const propertiest &, property_statust)
  Return the number of properties with given status.
 
bool  is_property_to_check (property_statust)
  Return true if the status is NOT_CHECKED or UNKNOWN.
 
bool  has_properties_to_check (const propertiest &properties)
  Return true if there as a property with NOT_CHECKED or UNKNOWN status.
 
property_statust &  operator|= (property_statust &, property_statust const &)
  Update with the preference order.
 
property_statust &  operator&= (property_statust &, property_statust const &)
  Update with the preference order.
 
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.
 

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 class 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 class 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&=()

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|=()

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.

AltStyle によって変換されたページ (->オリジナル) /