properties.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Properties
 
Author: Daniel Kroening, Peter Schrammel
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_CHECKER_PROPERTIES_H
#define CPROVER_GOTO_CHECKER_PROPERTIES_H
 
#include <map>
 
#include <goto-programs/goto_program.h>
 
class abstract_goto_modelt;
class json_objectt;
class json_stream_objectt;
class xmlt;
 
enum class property_statust
{
  NOT_CHECKED,
  UNKNOWN,
  NOT_REACHABLE,
  PASS,
  FAIL,
  ERROR
};
 
std::string as_string(property_statust);
 
enum class resultt
{
  UNKNOWN,
  PASS,
  FAIL,
  ERROR
};
 
std::string as_string(resultt);
 
struct property_infot
{
  property_infot(
    goto_programt::const_targett pc,
    std::string description,
    property_statust status);
 
  goto_programt::const_targett pc;
 
  std::string description;
 
  property_statust status;
};
 
typedef std::map<irep_idt, property_infot> propertiest;
 
propertiest initialize_properties(const abstract_goto_modelt &);
 
void update_properties_from_goto_model(
  propertiest &properties,
  const abstract_goto_modelt &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 &);
 
int result_to_exit_code(resultt result);
 
std::size_t count_properties(const propertiest &, property_statust);
 
bool is_property_to_check(property_statust);
 
bool has_properties_to_check(const propertiest &properties);
 
property_statust &operator|=(property_statust &, property_statust const &);
property_statust &operator&=(property_statust &, property_statust const &);
resultt determine_result(const propertiest &properties);
 
#endif // CPROVER_GOTO_CHECKER_PROPERTIES_H