verification_result.h

Go to the documentation of this file.

// Copyright (c) 2023 Fotis Koutoulakis for Diffblue Ltd.

//  in a structured form.
 
#ifndef CPROVER_LIBCPROVER_CPP_VERIFICATION_RESULT_H
#define CPROVER_LIBCPROVER_CPP_VERIFICATION_RESULT_H
 
#include <map>
#include <memory>
#include <string>
#include <vector>
 
class dstringt;
typedef dstringt irep_idt;
 
struct property_infot;
using propertiest = std::map<irep_idt, property_infot>;
enum class resultt;
 
// The enumerations here mirror the ones in properties.h.
// The reason we do so is that we want to expose the same information
// to users of the API, without including (and therefore, exposing)
// CBMC internal headers.
 
enum class prop_statust
{
  NOT_CHECKED,
  UNKNOWN,
  NOT_REACHABLE,
  PASS,
  FAIL,
  ERROR
};
 
enum class verifier_resultt
{
  UNKNOWN,
  PASS,
  FAIL,
  ERROR
};
 
struct verification_resultt
{
  verification_resultt();
  verification_resultt(const verification_resultt &other);
  ~verification_resultt();
  verification_resultt &operator=(verification_resultt &&);
  verification_resultt &operator=(const verification_resultt &other);
 
  void set_result(resultt &result);
  void set_properties(propertiest &properties);
 
  verifier_resultt final_result() const;
  std::vector<std::string> get_property_ids() const;
  std::string get_property_description(const std::string &property_id) const;
  prop_statust get_property_status(const std::string &property_id) const;
 
private:
  class verification_result_implt;
  std::unique_ptr<verification_result_implt> _impl;
};
 
// Allow translation of `verifier_resultt` into a CPROVER_EXIT_CODES (so that
// they can be consistent across various tools using the API).
int verifier_result_to_exit_code(verifier_resultt result);
 
#endif // CPROVER_GOTO_CHECKER_VERIFICATION_RESULT_H