Adding a character at the end of a string. More...

#include <string_builtin_function.h>

Inheritance diagram for string_concat_char_builtin_functiont:

Collaboration diagram for string_concat_char_builtin_functiont:

Public Member Functions
	string_concat_char_builtin_functiont (const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
	Constructor from arguments of a function application. More...

std::optional< exprt >	eval (const std::function< exprt(const exprt &)> &get_value) const override
	Given a function `get_value` which gives a valuation to expressions, attempt to find the result of the builtin function. More...

std::string	name () const override

string_constraintst	constraints (string_constraint_generatort &generator, message_handlert &message_handlert) const override
	Set of constraints enforcing that `result` is the concatenation of `input` with `character`. More...

exprt	length_constraint () const override
	Constraint ensuring that the length of the strings are coherent with the function call. More...

Public Member Functions inherited from string_transformation_builtin_functiont
	string_transformation_builtin_functiont (exprt return_code, array_string_exprt result, array_string_exprt input, array_poolt &array_pool)

	string_transformation_builtin_functiont (const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
	Constructor from arguments of a function application. More...

std::optional< array_string_exprt >	string_result () const override

std::vector< array_string_exprt >	string_arguments () const override

bool	maybe_testing_function () const override
	Tells whether the builtin function can be a testing function, that is a function that does not return a string, for instance like `equals`, `indexOf` or `compare`. More...

Public Member Functions inherited from string_builtin_functiont
	string_builtin_functiont ()=delete

	string_builtin_functiont (const string_builtin_functiont &)=delete

virtual	~string_builtin_functiont ()=default

Public Attributes
exprt	character

Public Attributes inherited from string_transformation_builtin_functiont
array_string_exprt	result

array_string_exprt	input

Public Attributes inherited from string_builtin_functiont
exprt	return_code

Additional Inherited Members
Protected Member Functions inherited from string_builtin_functiont
	string_builtin_functiont (exprt return_code, array_poolt &array_pool)

Protected Attributes inherited from string_builtin_functiont
array_poolt &	array_pool

Detailed Description

Adding a character at the end of a string.

Definition at line 172 of file string_builtin_function.h.

Constructor & Destructor Documentation

◆ string_concat_char_builtin_functiont()

string_concat_char_builtin_functiont::string_concat_char_builtin_functiont	(	const exprt &	return_code,
		const std::vector< exprt > &	fun_args,
		array_poolt &	array_pool
	)

inline

Constructor from arguments of a function application.

The arguments in fun_args should be in order: an integer result.length, a character pointer &result[0], a string arg1 of type refined_string_typet, and a character.

Definition at line 182 of file string_builtin_function.h.

Member Function Documentation

◆ constraints()

string_constraintst string_concat_char_builtin_functiont::constraints	(	string_constraint_generatort &	generator,
		message_handlert &	message_handler
	)		const