api.h

Go to the documentation of this file.

// Author: Fotis Koutoulakis for Diffblue Ltd.
 
#ifndef CPROVER_LIBCPROVER_CPP_API_H
#define CPROVER_LIBCPROVER_CPP_API_H
 
#include <memory>
#include <string>
#include <vector>
 
// Forward declaration of API dependencies
struct api_session_implementationt;
 
// There has been a design decision to allow users to include all of
// the API headers by just including `api.h`, so we want to have an
// include for all the API headers below. If we get any auxiliary
// development tools complaining about the includes, please use
// a pragma like below to silence the warning (at least as long
// as the design principle is to be followed.)
 
#include "api_options.h" // IWYU pragma: keep
#include "verification_result.h" // IWYU pragma: keep

struct api_messaget;

const char *api_message_get_string(const api_messaget &message);

bool api_message_is_error(const api_messaget &message);

using api_call_back_contextt = void *;

using api_message_callbackt = void (*)(
  const api_messaget &message,
  api_call_back_contextt call_back_context);
 
// An object in the pattern of Session Facade - owning all of the memory
// the API is using and being responsible for the management of that.
struct api_sessiont
{
  // Initialising constructor
  api_sessiont();
  explicit api_sessiont(const api_optionst &options);
  ~api_sessiont(); // default constructed in the .cpp file

  void set_message_callback(
    api_message_callbackt callback,
    api_call_back_contextt context);

  void load_model_from_files(const std::vector<std::string> &files) const;
 
  // Run the verification engine against previously loaded model and return
  // results object pointer.
  std::unique_ptr<verification_resultt> verify_model() const;

  void drop_unused_functions() const;

  void validate_goto_model() const;

  std::unique_ptr<std::string> get_api_version() const;

  std::unique_ptr<verification_resultt> run_verifier() const;

  void read_goto_binary(std::string &file) const;

  bool is_goto_binary(std::string &file) const;
 
private:
  std::unique_ptr<api_session_implementationt> implementation;

  bool preprocess_model() const;
};
 
#endif