CBMC
Loading...
Searching...
No Matches
Functions
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.
 
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)
 
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.
 
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.
 
bool  is_property_to_check (property_statust status)
  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 &a, property_statust const &b)
  Update with the preference order.
 
property_statust &  operator&= (property_statust &a, property_statust const &b)
  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.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.

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