string_builder Class Reference

Helper class for building and manipulating string expressions in Python frontend Handles null-termination, character extraction, and string concatenation. More...

#include <string_builder.h>

Public Member Functions
	string_builder (python_converter &converter, string_handler *handler)
exprt	make_null_terminator ()
	Create a null terminator character constant.
exprt	make_char_constant (unsigned char ch)
	Create a character constant from a byte value.
std::vector< exprt >	extract_string_chars (const exprt &expr, const nlohmann::json &json_node=nlohmann::json())
	Extract characters from an expression, stopping at null terminator Returns a vector of character expressions (without null terminator).
exprt	build_null_terminated_string (const std::vector< exprt > &chars)
	Create a null-terminated string array from a vector of character expressions.
exprt	build_string_literal (const std::string &str)
	Create a null-terminated string from a std::string.
exprt	build_byte_string (const std::vector< uint8_t > &bytes)
	Create a null-terminated string from a vector of bytes.
exprt	ensure_null_terminated_string (exprt &e)
	Ensure an expression is a null-terminated string Converts single characters or promotes to proper string arrays.
exprt	concatenate_strings (const exprt &lhs, const exprt &rhs, const nlohmann::json &left=nlohmann::json(), const nlohmann::json &right=nlohmann::json())
	Concatenate two string expressions with proper null-termination.
exprt	handle_string_repetition (exprt &lhs, exprt &rhs)
exprt	build_raw_byte_array (const std::vector< uint8_t > &bytes)
	Create a raw byte array without null termination (for Python bytes literals).
exprt	concatenate_strings_via_c_function (const exprt &lhs, const exprt &rhs, const nlohmann::json &left)
exprt	build_runtime_str_conversion_call (const std::string &fn_name, const typet &arg_type, const exprt &arg)
	Build a side-effect call to a char *fn(arg_type) operational model.
exprt	build_runtime_str_join_call (const exprt &separator, const exprt &list_expr)
	Build a side-effect call to the runtime __python_str_join operational model.

Detailed Description

Helper class for building and manipulating string expressions in Python frontend Handles null-termination, character extraction, and string concatenation.

Constructor & Destructor Documentation

string_builder()

string_builder::string_builder ( python_converter & converter, string_handler * handler )

explicit

Member Function Documentation

build_byte_string()

exprt string_builder::build_byte_string

(

const std::vector< uint8_t > &

bytes

)

Create a null-terminated string from a vector of bytes.

build_null_terminated_string()

exprt string_builder::build_null_terminated_string

(

const std::vector< exprt > &

chars

)

Create a null-terminated string array from a vector of character expressions.

build_raw_byte_array()

exprt string_builder::build_raw_byte_array

(

const std::vector< uint8_t > &

bytes

)

Create a raw byte array without null termination (for Python bytes literals).

build_runtime_str_conversion_call()

exprt string_builder::build_runtime_str_conversion_call	(	const std::string &	fn_name,
		const typet &	arg_type,
		const exprt &	arg )

Build a side-effect call to a char *fn(arg_type) operational model.

Looks up (or lazily creates) the function symbol for fn_name with the signature char *fn_name(arg_type) and returns a side_effect_expr_function_callt invoking it with arg. Used to dispatch str(int_var), str(float_var), str(bool_var) to the matching __python_*_to_str model at runtime.

build_runtime_str_join_call()

exprt string_builder::build_runtime_str_join_call	(	const exprt &	separator,
		const exprt &	list_expr )

Build a side-effect call to the runtime __python_str_join operational model.

separator is decayed to const char * and list_expr is passed as __ESBMC_PyListObj * (taking the address if needed). Used by handle_str_join when compile-time folding of the iterable fails.

build_string_literal()

exprt string_builder::build_string_literal

(

const std::string &

str

)

Create a null-terminated string from a std::string.

concatenate_strings()

exprt string_builder::concatenate_strings	(	const exprt &	lhs,
		const exprt &	rhs,
		const nlohmann::json &	left = nlohmann::json(),
		const nlohmann::json &	right = nlohmann::json() )

Concatenate two string expressions with proper null-termination.

concatenate_strings_via_c_function()

exprt string_builder::concatenate_strings_via_c_function	(	const exprt &	lhs,
		const exprt &	rhs,
		const nlohmann::json &	left )

ensure_null_terminated_string()

exprt string_builder::ensure_null_terminated_string

(

exprt &

e

)

Ensure an expression is a null-terminated string Converts single characters or promotes to proper string arrays.

extract_string_chars()

std::vector< exprt > string_builder::extract_string_chars	(	const exprt &	expr,
		const nlohmann::json &	json_node = nlohmann::json() )

Extract characters from an expression, stopping at null terminator Returns a vector of character expressions (without null terminator).

handle_string_repetition()

exprt string_builder::handle_string_repetition	(	exprt &	lhs,
		exprt &	rhs )

make_char_constant()

exprt string_builder::make_char_constant

(

unsigned char

ch

)

Create a character constant from a byte value.

make_null_terminator()

exprt string_builder::make_null_terminator

(

)

Create a null terminator character constant.

---

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

• src/python-frontend/string/string_builder.h
• src/python-frontend/string/string_builder.cpp