property_report.h

Go to the documentation of this file.

#ifndef CPROVER_ESBMC_PROPERTY_REPORT_H
#define CPROVER_ESBMC_PROPERTY_REPORT_H
 
#include <goto-programs/property_verdict.h>
 
#include <functional>
#include <map>
#include <set>
#include <string>
#include <vector>

struct property_rowt
{
  std::string id;
  std::string file;
  std::string function;
  std::string description;
  std::string note;
  unsigned line = 0;
  unsigned column = 0;
  unsigned instruction = 0;
  expr2tc condition;
  bool library = false;
  property_verdictt verdict = property_verdictt::NotChecked;
};

struct property_countst
{
  size_t passed = 0;
  size_t failed = 0;
  size_t unknown = 0;
  size_t not_checked = 0;
  size_t unreached = 0;
  size_t id_width = 0;
  size_t line_width = 0;

  bool anything_decided() const
  {
    return passed > 0 || failed > 0 || unknown > 0;
  }
};
 
property_countst count_properties(const std::vector<property_rowt> &rows);

extern const char *const unreached_claim_note;

const char *verdict_label(property_verdictt);
 
class goto_functionst;

std::set<std::string>
collect_library_assertion_files(const goto_functionst &goto_functions);

std::vector<property_rowt> build_property_rows(
  const std::map<std::string, property_resultt> &verdicts,
  const std::set<std::string> &library_files,
  const std::function<std::string(const expr2tc &)> &render_condition = {});
 
#endif