1// Author: Fotis Koutoulakis for Diffblue Ltd.
3#ifndef CPROVER_LIBCPROVER_CPP_API_H
4#define CPROVER_LIBCPROVER_CPP_API_H
10// Forward declaration of API dependencies
13// There has been a design decision to allow users to include all of
14// the API headers by just including `api.h`, so we want to have an
15// include for all the API headers below. If we get any auxiliary
16// development tools complaining about the includes, please use
17// a pragma like below to silence the warning (at least as long
18// as the design principle is to be followed.)
54// An object in the pattern of Session Facade - owning all of the memory
55// the API is using and being responsible for the management of that.
58 // Initialising constructor
75 // Run the verification engine against previously loaded model and return
76 // results object pointer.
77 std::unique_ptr<verification_resultt>
verify_model()
const;
90 std::unique_ptr<verification_resultt>
run_verifier()
const;
bool api_message_is_error(const api_messaget &message)
const char * api_message_get_string(const api_messaget &message)
Given a api_message, this function returns that message expressed as a C language string.
void(*)(const api_messaget &message, api_call_back_contextt call_back_context) api_message_callbackt
The type of call back for feedback of status information and results.
void * api_call_back_contextt
The type of pointers to contextual data passed to the api_message_callback functions.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
std::unique_ptr< std::string > get_api_version() const
A simple API version information function.
std::unique_ptr< verification_resultt > run_verifier() const
Process the model by running symex and the decision procedure.
bool preprocess_model() const
Implement necessary transformations to reduce model to symex-ready-GOTO, before being fed to symex.
void load_model_from_files(const std::vector< std::string > &files) const
Load a goto_model from a given vector of filenames.
bool is_goto_binary(std::string &file) const
True if file is goto-binary.
std::unique_ptr< verification_resultt > verify_model() const
void set_message_callback(api_message_callbackt callback, api_call_back_contextt context)
void drop_unused_functions() const
Drop unused functions from the loaded goto_model simplifying it.
void validate_goto_model() const
Validate the loaded goto model.
std::unique_ptr< api_session_implementationt > implementation
void read_goto_binary(std::string &file) const
Read a goto-binary from a given filename.
Interface for the various verification engines providing results.