python_exception_handler Class Reference

Handles Python exception-related statement conversion. More...

#include <python_exception_handler.h>

Public Member Functions
	python_exception_handler (python_converter &converter, type_handler &type_handler)
void	get_try_statement (const nlohmann::json &element, codet &block)
	Convert a Python try/except block.
void	get_raise_statement (const nlohmann::json &element, codet &block)
	Convert a Python raise statement.
void	get_except_handler_statement (const nlohmann::json &element, codet &block)
	Convert a Python except-handler clause.
void	emit_catch_block (const nlohmann::json &element, const nlohmann::json &type_node, codet &block)
void	handle_list_assertion (const nlohmann::json &element, const exprt &test, code_blockt &block, const std::function< void(code_assertt &)> &attach_assert_message)
	Emit a truthiness assertion on a list value.
void	handle_function_call_assertion (const nlohmann::json &element, const exprt &func_call_expr, bool is_negated, code_blockt &block, const std::function< void(code_assertt &)> &attach_assert_message)
	Emit an assertion whose condition depends on a function-call result.
exprt	gen_exception_raise (const std::string &exc, const std::string &message) const
	Build a cpp-throw side-effect expression for a named Python exception.

Static Public Member Functions
static bool	body_has_escaping_control_flow (const nlohmann::json &node, bool in_loop)
	True if node contains a return/break/continue that would transfer control out of an enclosing try (used to refuse try/finally shapes whose appended finally would be skipped).
static bool	escape_in_nested_cleanup_scope (const nlohmann::json &node, bool in_loop)
	True if an escaping return/break/continue sits inside a nested try or with, whose own cleanup must run before this finally.
static bool	escape_in_nested_cleanup_children (const nlohmann::json &node, bool in_loop)
	escape_in_nested_cleanup_scope's walk over a statement's child bodies.

Detailed Description

Handles Python exception-related statement conversion.

Centralises all try/except/raise statement conversion and exception expression helpers that were previously scattered across python_converter and function_call_expr. Keeping exception logic here makes python_converter easier to read and makes it straightforward to extend exception support in one place.

Constructor & Destructor Documentation

python_exception_handler()

python_exception_handler::python_exception_handler ( python_converter & converter, type_handler & type_handler )

explicit

Member Function Documentation

body_has_escaping_control_flow()

bool python_exception_handler::body_has_escaping_control_flow ( const nlohmann::json & node, bool in_loop )

static

True if node contains a return/break/continue that would transfer control out of an enclosing try (used to refuse try/finally shapes whose appended finally would be skipped).

in_loop tracks loop nesting so that break/continue captured by a nested loop are not counted.

emit_catch_block()

void python_exception_handler::emit_catch_block	(	const nlohmann::json &	element,
		const nlohmann::json &	type_node,
		codet &	block )

escape_in_nested_cleanup_children()

bool python_exception_handler::escape_in_nested_cleanup_children ( const nlohmann::json & node, bool in_loop )

static

escape_in_nested_cleanup_scope's walk over a statement's child bodies.

escape_in_nested_cleanup_scope()

bool python_exception_handler::escape_in_nested_cleanup_scope ( const nlohmann::json & node, bool in_loop )

static

True if an escaping return/break/continue sits inside a nested try or with, whose own cleanup must run before this finally.

Duplicating this finally there would order the two wrongly, so such shapes are refused.

gen_exception_raise()

exprt python_exception_handler::gen_exception_raise	(	const std::string &	exc,
		const std::string &	message ) const

Build a cpp-throw side-effect expression for a named Python exception.

Parameters

exc	Exception class name, e.g. "TypeError".
message	Human-readable message string.

Returns

A side_effect_exprt of type cpp-throw.

get_except_handler_statement()

void python_exception_handler::get_except_handler_statement	(	const nlohmann::json &	element,
		codet &	block )

Convert a Python except-handler clause.

Creates a symbol for the bound exception variable (if any), processes the handler body and prepends the declaration.

Parameters

element	The AST node with _type == "ExceptHandler".
block	The target code block to receive the converted statement.

get_raise_statement()

void python_exception_handler::get_raise_statement	(	const nlohmann::json &	element,
		codet &	block )

Convert a Python raise statement.

Raises are lowered to side-effect cpp-throw expressions. AssertionError is special-cased to a code_assertt(false) for cleaner verification output.

Parameters

element	The AST node with _type == "Raise".
block	The target code block to receive the converted statement.

get_try_statement()

void python_exception_handler::get_try_statement	(	const nlohmann::json &	element,
		codet &	block )

Convert a Python try/except block.

Handles the special case where the try body contains a failed import (module_not_found flag set by the pre-processor) and statically selects only the ImportError handler body. For all other cases the full cpp-catch IR node is produced.

Parameters

element	The AST node with _type == "Try".
block	The target code block to receive the converted statement.

handle_function_call_assertion()

void python_exception_handler::handle_function_call_assertion	(	const nlohmann::json &	element,
		const exprt &	func_call_expr,
		bool	is_negated,
		code_blockt &	block,
		const std::function< void(code_assertt &)> &	attach_assert_message )

Emit an assertion whose condition depends on a function-call result.

Creates a temporary boolean variable, executes the call and asserts the result (or its negation when is_negated is true). For functions that return None the call is executed and then False is asserted.

Parameters

element	AST node used for location information.
func_call_expr	The function-call expression.
is_negated	True when the test was wrapped in a UnaryOp Not.
block	Target block.
attach_assert_message	Callback to set the assertion comment.

handle_list_assertion()

void python_exception_handler::handle_list_assertion	(	const nlohmann::json &	element,
		const exprt &	test,
		code_blockt &	block,
		const std::function< void(code_assertt &)> &	attach_assert_message )

Emit a truthiness assertion on a list value.

Materialises the list (handling function-call RHS), calls __ESBMC_list_size and asserts size > 0.

Parameters

element	AST node used for location information.
test	Expression representing the list.
block	Target block.
attach_assert_message	Callback that sets the comment on the produced code_assertt.

---

The documentation for this class was generated from the following files:

• src/python-frontend/exception/python_exception_handler.h
• src/python-frontend/exception/python_exception_handler.cpp