#include <string_concatenation_builtin_function.h>

Inheritance diagram for string_concatenation_builtin_functiont:

Collaboration diagram for string_concatenation_builtin_functiont:

Public Member Functions
	string_concatenation_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::vector< mp_integer >	eval (const std::vector< mp_integer > &input1_value, const std::vector< mp_integer > &input2_value, const std::vector< mp_integer > &args_value) const override
	Evaluate the result from a concrete valuation of the arguments. More...

std::string	name () const override

string_constraintst	constraints (string_constraint_generatort &generator, message_handlert &message_handler) const override
	Add constraints ensuring that the value of result expression of the builtin function corresponds to the value of the function call. 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_insertion_builtin_functiont
	string_insertion_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

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_handler) const override
	Constraints ensuring the `result` corresponds to `input1` where we inserted `input2` at position `offset` given by the first argument. More...

exprt	length_constraint () 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

Additional Inherited Members
Public Attributes inherited from string_insertion_builtin_functiont
array_string_exprt	result

array_string_exprt	input1

array_string_exprt	input2

std::vector< exprt >	args

Public Attributes inherited from string_builtin_functiont
exprt	return_code

Protected Member Functions inherited from string_insertion_builtin_functiont
	string_insertion_builtin_functiont (const exprt &return_code, array_poolt &array_pool)

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

Definition at line 17 of file string_concatenation_builtin_function.h.

Constructor & Destructor Documentation

◆ string_concatenation_builtin_functiont()

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

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, a string arg2 of type refined_string_typet, optionally followed by an integer start and an integer end.

Definition at line 16 of file string_concatenation_builtin_function.cpp.

Member Function Documentation

◆ constraints()

string_constraintst string_concatenation_builtin_functiont::constraints	(	string_constraint_generatort &	,
		message_handlert &
	)		const

overridevirtual

Add constraints ensuring that the value of result expression of the builtin function corresponds to the value of the function call.

The constraints are only added when deemed necessary, i.e. when maybe_testing_function() returns true, or when testing function depends on the result of this function. This logic is implemented in add_constraints().

Implements string_builtin_functiont.

Definition at line 212 of file string_concatenation_builtin_function.cpp.

◆ eval()

std::vector< mp_integer > string_concatenation_builtin_functiont::eval	(	const std::vector< mp_integer > &	input1_value,
		const std::vector< mp_integer > &	input2_value,
		const std::vector< mp_integer > &	args_value
	)		const