1// Author: Fotis Koutoulakis for Diffblue Ltd, 2023.
7// The following type is cloning two types from the `util/exception_utils.h` and
8// `util/invariant.h` files.
10// The reason we need to do this is as follows: We have a fundamental constraint
11// in that we don't want to export internal headers to the clients, and our
12// current build system architecture on the C++ end doesn't allow us to do so.
14// At the same time, we want to allow the Rust API to be able to catch at the
15// shimlevel the errors generated within CBMC, which are C++ types (and
16// subtypes of those), and so because of the mechanism that cxx.rs uses, we
17// need to have thetypes present at compilation time (an incomplete type won't
20// This is the best way that we have currently to be have the type definitions
21// around so that the exception handling code knows what our exceptions look
22// like (especially given that they don't inherit from `std::exception`), so
23// that our system compiles and is functional, without needing include chains
24// outside of the API implementation (which we can't expose as well).
26// This should mirror the definition in `util/invariant.h`.
59// This is needed here because the original definition is in the file
60// <util/exception_utils.h> which is including <util/source_location.h>, which
61// being an `irep` is a no-go for our needs as we will need to expose internal
69 virtual std::string
what()
const;
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Base class for exceptions thrown in the cprover project.
virtual ~cprover_exception_baset()=default
virtual std::string what() const
A human readable description of what went wrong.
cprover_exception_baset(std::string reason)
This constructor is marked protected to ensure this class isn't used directly.
std::string reason
The reason this exception was generated.
A logic error, augmented with a distinguished field to hold a backtrace.
const std::string backtrace
const std::string condition
virtual ~invariant_failedt()=default
virtual std::string what() const noexcept
const std::string function