#include <api.h>

Collaboration diagram for api_sessiont:

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