exception_globals Namespace Reference

Global symbols that carry the in-flight exception across the GOTO program once throw/catch dispatch is lowered to ordinary control flow (issue #5075). More...

Enumerations
enum	terminate_reasont : unsigned {   terminate_reason_generic = 0 , terminate_reason_uncaught = 1 , terminate_reason_noexcept = 2 , terminate_reason_exception_spec = 3 ,   terminate_reason_no_active = 4 , terminate_reason_unwinding = 5 }

Variables
constexpr const char *	thrown_id = "c:@__ESBMC_exc_thrown"
constexpr const char *	typeid_id = "c:@__ESBMC_exc_typeid"
constexpr const char *	value_id = "c:@__ESBMC_exc_value"
constexpr const char *	uncaught_count_id = "c:@__ESBMC_exc_uncaught_count"
constexpr const char *	site_id = "c:@__ESBMC_exc_site"
constexpr const char *	terminate_reason_id = "c:@__ESBMC_exc_terminate_reason"
constexpr unsigned	unattributed_site = 0
	Site id for a raise no property may be attributed to: one in a hidden operational model, in an unreachable function, or taken by a handler in its own function.
constexpr const char *	push_handled_id = "c:@F@__ESBMC_push_handled_exception"
constexpr const char *	pop_handled_id = "c:@F@__ESBMC_pop_handled_exception"
constexpr const char *	rethrow_current_id

Detailed Description

Global symbols that carry the in-flight exception across the GOTO program once throw/catch dispatch is lowered to ordinary control flow (issue #5075).

Together they replace the imperative stack_catch/thrown_obj_map state held in goto_symext: the lowering pass arms them at a throw, and handler landing pads read them in guarded gotos.

$esbmc_exc_thrown : _Bool — is an exception currently propagating? $esbmc_exc_typeid : size_t — dynamic type id of the thrown object, from exception_typeidt (0 == none). $esbmc_exc_value : void* — pointer to the most-derived thrown object, so handlers can bind/slice it. $esbmc_exc_uncaught_count : size_t — number of exceptions thrown (or rethrown) in this thread that have not yet entered their matching handler; backs std::uncaught_exception(s) ([except.uncaught]). $esbmc_exc_site : size_t — id of the raise the in-flight exception came from, so the uncaught-exception property can name the raising statement when a type is raised from several (issue #7769). 0 means "no attributable site", which the residual check covers. $esbmc_exc_terminate_reason : size_t — classification of the terminate point that routed into std::terminate(), so the default handler can keep the original diagnostic (e.g. noexcept violation vs uncaught exception).

The typeid is a size_t to line up with the Python frontend's existing PyObject.type_id field and with exception_typeidt's unsigned ids; the value is a void* the handler static_casts to the caught type.

Enumeration Type Documentation

terminate_reasont

enum exception_globals::terminate_reasont : unsigned

Enumerator
terminate_reason_generic
terminate_reason_uncaught
terminate_reason_noexcept
terminate_reason_exception_spec
terminate_reason_no_active
terminate_reason_unwinding

Variable Documentation

pop_handled_id

const char* exception_globals::pop_handled_id = "c:@F@__ESBMC_pop_handled_exception"

constexpr

push_handled_id

const char* exception_globals::push_handled_id = "c:@F@__ESBMC_push_handled_exception"

constexpr

rethrow_current_id

const char* exception_globals::rethrow_current_id

constexpr

Initial value:

=
  "c:@F@__ESBMC_rethrow_current_exception"

site_id

const char* exception_globals::site_id = "c:@__ESBMC_exc_site"

constexpr

terminate_reason_id

const char* exception_globals::terminate_reason_id = "c:@__ESBMC_exc_terminate_reason"

constexpr

thrown_id

const char* exception_globals::thrown_id = "c:@__ESBMC_exc_thrown"

constexpr

typeid_id

const char* exception_globals::typeid_id = "c:@__ESBMC_exc_typeid"

constexpr

unattributed_site

unsigned exception_globals::unattributed_site = 0

constexpr

Site id for a raise no property may be attributed to: one in a hidden operational model, in an unreachable function, or taken by a handler in its own function.

Never assigned to a real site, so a per-site check never matches it and the residual is what covers such a raise.

uncaught_count_id

const char* exception_globals::uncaught_count_id = "c:@__ESBMC_exc_uncaught_count"

constexpr

value_id

const char* exception_globals::value_id = "c:@__ESBMC_exc_value"

constexpr