remove_exceptions.h File Reference

#include <set>
#include <vector>
#include <util/irep/irep_idt.h>

Include dependency graph for remove_exceptions.h:

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

Go to the source code of this file.

Functions
void	remove_exceptions (goto_functionst &goto_functions, contextt &context, const namespacet &ns, const std::set< irep_idt > &unreported={}, const std::vector< irep_idt > &checked={})
	Lower C++/Python exception dispatch (THROW/CATCH) into ordinary guarded control flow over the global exception state (issue #5075).
bool	checks_exception (const exception_typeidt &types, const irep_idt &type, const std::vector< irep_idt > &checked)
	Whether type is a subtype of a type in checked, or checked is empty.
std::vector< irep_idt >	python_checked_exceptions (const optionst &options)
	The exception types –python-check-exceptions lists, or none without it.

Function Documentation

checks_exception()

bool checks_exception	(	const exception_typeidt &	types,
		const irep_idt &	type,
		const std::vector< irep_idt > &	checked )

Whether type is a subtype of a type in checked, or checked is empty.

python_checked_exceptions()

std::vector< irep_idt > python_checked_exceptions

(

const optionst &

options

)

The exception types –python-check-exceptions lists, or none without it.

remove_exceptions()

void remove_exceptions	(	goto_functionst &	goto_functions,
		contextt &	context,
		const namespacet &	ns,
		const std::set< irep_idt > &	unreported = {},
		const std::vector< irep_idt > &	checked = {} )

Lower C++/Python exception dispatch (THROW/CATCH) into ordinary guarded control flow over the global exception state (issue #5075).

A throw is rewritten to arm the $esbmc_exc_{thrown,typeid,value} globals (see exception_globals.h) and branch, in catch-declaration order, to the first matching handler — the match expressed as a guard typeid in concrete_subtype_ids(C) (see exception_typeidt) over a symbolic type-id, with catch (...) as an unconditional branch.

Scope (whole-program, all-or-nothing — anything outside it is reported as unsupported, since this is the only exception path):

• C++ class and primitive throws; reference, value (with single-inheritance slicing), pointer and void* catches, and catch-all;
• nested try regions with innermost-out propagation;
• inter-procedural propagation through direct and indirect calls, and rethrow;
• uncaught detection at main and __ESBMC_main (incl. static-init throws);
• Python try/except/raise via the same machinery. A small residual is rejected as unsupported (e.g. concurrent programs that use exceptions, –function isolated verification, std::bad_exception by value); the pass errors when it declines (report_unsupported).

Run before goto_partial_inline. This is the only exception path — the legacy imperative symex dispatch was removed once the lowered subset covered the corpus (#5075).

An uncaught exception whose type is in unreported ends the run without a property, as –python-ignore-assertions wants for AssertionError. With checked non-empty, so does one whose type is not a subtype of a type in checked, as –python-check-exceptions wants. An operational-model assert whose comment names such a type ("KeyError: ...") becomes an assume.