property_verdict.h

Go to the documentation of this file.

#ifndef CPROVER_GOTO_PROGRAMS_PROPERTY_VERDICT_H
#define CPROVER_GOTO_PROGRAMS_PROPERTY_VERDICT_H
 
#include <goto-programs/goto_program.h>
#include <util/irep/location.h>
 
#include <atomic>
#include <cstddef>
#include <map>
#include <mutex>
#include <set>
#include <string>
 
class optionst;

enum class property_verdictt
{
  NotChecked = 0,
  Passed = 1,
  Unknown = 2,
  Failed = 3
};

struct property_locationt
{
  std::string file;
  std::string function;
  std::string description;
  unsigned line = 0;
  unsigned column = 0;
  unsigned instruction = 0;
  expr2tc condition;
};

property_locationt property_location(
  const goto_programt::instructiont &pc,
  const std::string &description);

std::string property_key(
  const goto_programt::instructiont &pc,
  const std::string &description);

struct property_resultt
{
  property_verdictt verdict;
  std::string note;
  property_locationt loc;
};

class property_verdict_tablet
{
public:
  void record(
    const std::string &property,
    property_verdictt verdict,
    const property_locationt &loc,
    const std::string &note = "");

  void promote_unchecked_to_passed();

  void note_incomplete();

  void begin_round();

  void complete_round()
  {
    incomplete = false;
  }

  bool is_incomplete() const
  {
    return incomplete;
  }

  bool all_passed() const;

  std::size_t size() const;

  bool has_violation() const
  {
    return violation;
  }

  std::map<std::string, property_resultt> snapshot() const;

  void clear();
 
private:
  mutable std::mutex mutex;
  std::map<std::string, property_resultt> results;
  std::set<std::string> recorded_this_round;
  std::atomic<bool> violation{false};
  std::atomic<bool> incomplete{false};
};

bool withholds_proofs(const optionst &options);
 
#endif