#ifndef ESBMC_EXCEPTION
#define ESBMC_EXCEPTION

// ESBMC model for <exception>.
//
// Keep this header to the standard C++ surface.  Do not mirror libstdc++ or
// libc++ private ABI details here; non-template behavior is provided by ESBMC
// model hooks and the exception lowering machinery.

#if __cplusplus >= 201103L
#  define _ESBMC_NOEXCEPT noexcept
#  include <type_traits> // std::enable_if, std::decay for throw_with_nested
#else
#  define _ESBMC_NOEXCEPT throw()
#endif

extern "C" void *__ESBMC_current_exception_raw(void);
extern "C" void __ESBMC_rethrow_exception_raw(void *);

namespace std
{

class exception
{
public:
  exception() _ESBMC_NOEXCEPT
  {
  }

  exception(const exception &) _ESBMC_NOEXCEPT
  {
  }

  exception &operator=(const exception &) _ESBMC_NOEXCEPT
  {
    return *this;
  }

  virtual ~exception() _ESBMC_NOEXCEPT
  {
  }

  virtual const char *what() const _ESBMC_NOEXCEPT
  {
    return "std::exception";
  }
};

class bad_exception : public exception
{
public:
  bad_exception() _ESBMC_NOEXCEPT
  {
  }

  bad_exception(const bad_exception &) _ESBMC_NOEXCEPT
  {
  }

  bad_exception &operator=(const bad_exception &) _ESBMC_NOEXCEPT
  {
    return *this;
  }

  virtual ~bad_exception() _ESBMC_NOEXCEPT
  {
  }

  virtual const char *what() const _ESBMC_NOEXCEPT
  {
    return "std::bad_exception";
  }
};

typedef void (*terminate_handler)();

void terminate() _ESBMC_NOEXCEPT;

} // namespace std

namespace std
{

terminate_handler set_terminate(terminate_handler) _ESBMC_NOEXCEPT;
terminate_handler get_terminate() _ESBMC_NOEXCEPT;
void terminate() _ESBMC_NOEXCEPT;

#if __cplusplus < 201703L
typedef void (*unexpected_handler)();

unexpected_handler set_unexpected(unexpected_handler) _ESBMC_NOEXCEPT;
unexpected_handler get_unexpected() _ESBMC_NOEXCEPT;

void unexpected();
#endif

#if __cplusplus < 202002L
bool uncaught_exception() _ESBMC_NOEXCEPT;
#endif

#if __cplusplus >= 201703L
int uncaught_exceptions() _ESBMC_NOEXCEPT;
#endif

#if __cplusplus >= 201103L
class exception_ptr
{
  void *object;

  friend exception_ptr current_exception() _ESBMC_NOEXCEPT;
  friend void rethrow_exception(exception_ptr);
  friend bool
  operator==(const exception_ptr &, const exception_ptr &) _ESBMC_NOEXCEPT;

public:
  exception_ptr() _ESBMC_NOEXCEPT : object(0)
  {
  }

  exception_ptr(decltype(nullptr)) _ESBMC_NOEXCEPT : object(0)
  {
  }

  explicit operator bool() const _ESBMC_NOEXCEPT
  {
    return object != 0;
  }
};

inline bool
operator==(const exception_ptr &lhs, const exception_ptr &rhs) _ESBMC_NOEXCEPT
{
  return lhs.object == rhs.object;
}

inline bool
operator!=(const exception_ptr &lhs, const exception_ptr &rhs) _ESBMC_NOEXCEPT
{
  return !(lhs == rhs);
}

exception_ptr current_exception() _ESBMC_NOEXCEPT;
void rethrow_exception(exception_ptr);

template <class E>
exception_ptr make_exception_ptr(E e) _ESBMC_NOEXCEPT
{
  try
  {
    throw e;
  }
  catch (...)
  {
    return current_exception();
  }
}

class nested_exception
{
  exception_ptr ptr;

public:
  nested_exception() _ESBMC_NOEXCEPT : ptr(current_exception())
  {
  }

  nested_exception(const nested_exception &) _ESBMC_NOEXCEPT
    : ptr(current_exception())
  {
  }

  nested_exception &operator=(const nested_exception &) _ESBMC_NOEXCEPT
  {
    return *this;
  }

  virtual ~nested_exception() _ESBMC_NOEXCEPT
  {
  }

  void rethrow_nested() const
  {
    if (ptr)
      rethrow_exception(ptr);

    terminate();
  }

  exception_ptr nested_ptr() const _ESBMC_NOEXCEPT
  {
    return ptr;
  }
};

// A type that publicly derives from both the user type T and nested_exception,
// so a `catch` can bind it as T (or std::exception) and rethrow_if_nested can
// recover the captured exception. nested_exception's default constructor
// captures current_exception() at construction ([except.nested]).
template <class T>
struct __ESBMC_nested_with : public T, public nested_exception
{
  explicit __ESBMC_nested_with(const T &t) : T(t)
  {
  }
};

// throw_with_nested(t): when decay_t<T> is a class not already derived from
// nested_exception, throw the combined type; otherwise throw t unchanged
// ([except.nested]/1). is_class/is_base_of via clang builtins (type_traits here
// provides only enable_if/decay).
template <class T>
typename enable_if<
  __is_class(typename decay<T>::type) &&
  !__is_base_of(nested_exception, typename decay<T>::type)>::type
throw_with_nested(T &&t)
{
  throw __ESBMC_nested_with<typename decay<T>::type>(static_cast<T &&>(t));
}

template <class T>
typename enable_if<!(
  __is_class(typename decay<T>::type) &&
  !__is_base_of(nested_exception, typename decay<T>::type))>::type
throw_with_nested(T &&t)
{
  throw static_cast<T &&>(t);
}

// rethrow_if_nested(e): if e is (dynamically) a nested_exception, rethrow its
// captured exception; otherwise do nothing ([except.nested]/2). The dynamic_cast
// is only well-formed for a polymorphic class, so non-polymorphic operands take
// the no-op overload.
template <class E>
typename enable_if<__is_class(E) && __is_polymorphic(E)>::type
rethrow_if_nested(const E &e)
{
  const nested_exception *n = dynamic_cast<const nested_exception *>(&e);
  if (n && n->nested_ptr())
    n->rethrow_nested();
}

template <class E>
typename enable_if<!(__is_class(E) && __is_polymorphic(E))>::type
rethrow_if_nested(const E &)
{
}

#endif // __cplusplus >= 201103L

} // namespace std

namespace std
{

#if __cplusplus >= 201103L
inline exception_ptr current_exception() _ESBMC_NOEXCEPT
{
  exception_ptr ptr;
  ptr.object = __ESBMC_current_exception_raw();
  return ptr;
}

inline void rethrow_exception(exception_ptr ptr)
{
  __ESBMC_rethrow_exception_raw(ptr.object);
}
#endif

} // namespace std

#endif // ESBMC_EXCEPTION
