exception_globals.h File Reference

#include <util/irep/irep.h>

Include dependency graph for exception_globals.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

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

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

Functions
void	create_exception_state_symbols (contextt &context)
	Idempotently register the exception-state globals in context, zero-initialised (thrown=false, typeid=0, value=NULL, uncaught_count=0).

Variables
constexpr const char *	exception_globals::thrown_id = "c:@__ESBMC_exc_thrown"
constexpr const char *	exception_globals::typeid_id = "c:@__ESBMC_exc_typeid"
constexpr const char *	exception_globals::value_id = "c:@__ESBMC_exc_value"
constexpr const char *	exception_globals::uncaught_count_id = "c:@__ESBMC_exc_uncaught_count"
constexpr const char *	exception_globals::site_id = "c:@__ESBMC_exc_site"
constexpr const char *	exception_globals::terminate_reason_id = "c:@__ESBMC_exc_terminate_reason"
constexpr unsigned	exception_globals::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 *	exception_globals::push_handled_id = "c:@F@__ESBMC_push_handled_exception"
constexpr const char *	exception_globals::pop_handled_id = "c:@F@__ESBMC_pop_handled_exception"
constexpr const char *	exception_globals::rethrow_current_id

Function Documentation

create_exception_state_symbols()

void create_exception_state_symbols

(

contextt &

context

)

Idempotently register the exception-state globals in context, zero-initialised (thrown=false, typeid=0, value=NULL, uncaught_count=0).

If a symbol already exists — e.g. the operational-model std::uncaught_exceptions() pulled in __ESBMC_exc_uncaught_count as an extern declaration during library linking — its storage flags are upgraded in place (static, thread-local, zero-initialised) rather than left as a bare declaration. Safe to call once per run before lowering.