libcprover_rust 6.9.0

Rust API for CBMC and assorted CProver tools
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74

// Author Fotis Koutoulakis for Diffblue Ltd 2022.

#pragma once

#include <memory>
#include <stdexcept>
#include <string>

// NOLINTNEXTLINE(build/include)
#include "rust/cxx.h"
// NOLINTNEXTLINE(build/include)
#include "include/c_errors.h"

struct api_sessiont;
struct verification_resultt;
enum class verifier_resultt;
enum class prop_statust;

// Helper function
std::vector<std::string> const &
_translate_vector_of_string(rust::Vec<rust::String> elements);

// Exposure of the C++ object oriented API through free-standing functions.
std::unique_ptr<api_sessiont> new_api_session();
std::vector<std::string> const &get_messages();

// Exposure of verification result related functions.
verifier_resultt
get_verification_result(const std::unique_ptr<verification_resultt> &v);
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 &);
prop_statust get_property_status(
  const std::unique_ptr<verification_resultt> &,
  const std::string &);

// NOLINTNEXTLINE(readability/namespace)
namespace rust
{
// NOLINTNEXTLINE(readability/namespace)
namespace behavior
{
template <typename Try, typename Fail>
static void trycatch(Try &&func, Fail &&fail) noexcept
{
  try
  {
    func();
  }
  catch(const cprover_exception_baset &e)
  {
    fail(e.what());
  }
  catch(const invariant_failedt &i)
  {
    fail(i.what());
  }
  catch(const std::out_of_range &our)
  {
    fail(our.what());
  }
  catch(const std::exception &exc)
  {
    // collective catch-all for all exceptions that derive
    // from standard exception class.
    fail(exc.what());
  }
}

} // namespace behavior

} // namespace rust