CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
c_api.h
Go to the documentation of this file.
1// Author Fotis Koutoulakis for Diffblue Ltd 2022.
2
3#pragma once
4
5#include <memory>
6#include <stdexcept>
7#include <string>
8
9// NOLINTNEXTLINE(build/include)
10#include "rust/cxx.h"
11// NOLINTNEXTLINE(build/include)
12#include "include/c_errors.h"
13
14struct api_sessiont;
16enum class verifier_resultt;
17enum class prop_statust;
18
19// Helper function
20std::vector<std::string> const &
21_translate_vector_of_string(rust::Vec<rust::String> elements);
22
23// Exposure of the C++ object oriented API through free-standing functions.
24std::unique_ptr<api_sessiont> new_api_session();
25std::vector<std::string> const &get_messages();
26
27// Exposure of verification result related functions.
29get_verification_result(const std::unique_ptr<verification_resultt> &v);
30std::vector<std::string> const &
31get_property_ids(const std::unique_ptr<verification_resultt> &);
32std::string const &get_property_description(
33 const std::unique_ptr<verification_resultt> &,
34 const std::string &);
36 const std::unique_ptr<verification_resultt> &,
37 const std::string &);
38
39// NOLINTNEXTLINE(readability/namespace)
40namespace rust
41{
42// NOLINTNEXTLINE(readability/namespace)
43namespace behavior
44{
45template <typename Try, typename Fail>
46static void trycatch(Try &&func, Fail &&fail) noexcept
47{
48 try
49 {
50 func();
51 }
52 catch(const cprover_exception_baset &e)
53 {
54 fail(e.what());
55 }
56 catch(const invariant_failedt &i)
57 {
58 fail(i.what());
59 }
60 catch(const std::out_of_range &our)
61 {
62 fail(our.what());
63 }
64 catch(const std::exception &exc)
65 {
66 // collective catch-all for all exceptions that derive
67 // from standard exception class.
68 fail(exc.what());
69 }
70}
71
72} // namespace behavior
73
74} // namespace rust
std::vector< std::string > const & get_property_ids(const std::unique_ptr< verification_resultt > &)
std::string const & get_property_description(const std::unique_ptr< verification_resultt > &, const std::string &)
std::unique_ptr< api_sessiont > new_api_session()
prop_statust get_property_status(const std::unique_ptr< verification_resultt > &, const std::string &)
verifier_resultt get_verification_result(const std::unique_ptr< verification_resultt > &v)
std::vector< std::string > const & _translate_vector_of_string(rust::Vec< rust::String > elements)
std::vector< std::string > const & get_messages()
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class for exceptions thrown in the cprover project.
Definition c_errors.h:64
virtual std::string what() const
A human readable description of what went wrong.
A logic error, augmented with a distinguished field to hold a backtrace.
Definition c_errors.h:28
virtual std::string what() const noexcept
static void trycatch(Try &&func, Fail &&fail) noexcept
Definition c_api.h:46
Definition c_api.h:41
verifier_resultt