Loading...

Searching...

No Matches

Public Member Functions | Private Member Functions | Private Attributes | List of all members

api_sessiont Struct Reference

#include <api.h>

+ Collaboration diagram for api_sessiont:

[フレーム]

[legend]

Public Member Functions

api_sessiont ()

api_sessiont (const api_optionst &options)

~api_sessiont ()

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

Load a goto_model from a given vector of filenames.

std::unique_ptr< verification_resultt > verify_model () const

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< 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.

void read_goto_binary (std::string &file) const

Read a goto-binary from a given filename.

bool is_goto_binary (std::string &file) const

True if file is goto-binary.

Private Member Functions

bool preprocess_model () const

Implement necessary transformations to reduce model to symex-ready-GOTO, before being fed to symex.

Private Attributes

std::unique_ptr< api_session_implementationt > implementation

Detailed Description

Definition at line 56 of file api.h.

Constructor & Destructor Documentation

◆ api_sessiont() [1/2]

api_sessiont::api_sessiont ( )

Definition at line 49 of file api.cpp.

◆ api_sessiont() [2/2]

api_sessiont::api_sessiont ( const api_optionst & options )

explicit

Definition at line 53 of file api.cpp.

◆ ~api_sessiont()

api_sessiont::~api_sessiont ( )

default

Member Function Documentation

◆ drop_unused_functions()

void api_sessiont::drop_unused_functions ( ) const

Drop unused functions from the loaded goto_model simplifying it.

Definition at line 243 of file api.cpp.

◆ get_api_version()

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

A simple API version information function.

Definition at line 37 of file api.cpp.

◆ is_goto_binary()

bool api_sessiont::is_goto_binary ( std::string & file ) const

True if file is goto-binary.

Definition at line 173 of file api.cpp.

◆ load_model_from_files()

void api_sessiont::load_model_from_files ( const std::vector< std::string > & files ) const

Load a goto_model from a given vector of filenames.

Parameters: files A vector<string> containing the filenames to be loaded

Definition at line 136 of file api.cpp.

◆ preprocess_model()

bool api_sessiont::preprocess_model ( ) const

private

Implement necessary transformations to reduce model to symex-ready-GOTO, before being fed to symex.

Returns: The function returns true if it failed because CBMC produced an error.

Definition at line 178 of file api.cpp.

◆ read_goto_binary()

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

Read a goto-binary from a given filename.

Warning: Will error out if it reads a source file.

Definition at line 156 of file api.cpp.

◆ run_verifier()

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

Process the model by running symex and the decision procedure.

Returns: a unique_ptr to the verification_resultt summary.

Definition at line 223 of file api.cpp.

◆ set_message_callback()

void api_sessiont::set_message_callback ( api_message_callbackt callback,

api_call_back_contextt context

)

Parameters: callback A call back function to receive progress updates and success/failure statuses.

context A context pointer passed through to the callback function. This is used similarly to a capture in a lambda function.

Definition at line 128 of file api.cpp.

◆ validate_goto_model()

void api_sessiont::validate_goto_model ( ) const

Validate the loaded goto model.

Definition at line 258 of file api.cpp.

◆ verify_model()

std::unique_ptr< verification_resultt > api_sessiont::verify_model ( ) const

Definition at line 143 of file api.cpp.

Member Data Documentation

◆ implementation

std::unique_ptr<api_session_implementationt> api_sessiont::implementation

private

Definition at line 100 of file api.h.

The documentation for this struct was generated from the following files:

/home/runner/work/cbmc/cbmc/src/libcprover-cpp/api.h
/home/runner/work/cbmc/cbmc/src/libcprover-cpp/api.cpp