String inserting a string into another one. More...

#include <string_insertion_builtin_function.h>

Inheritance diagram for string_insertion_builtin_functiont:

Collaboration diagram for string_insertion_builtin_functiont:

Public Member Functions
	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

virtual 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
	Evaluate the result from a concrete valuation of the arguments. 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_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

Public Attributes
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
	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)

Additional Inherited Members
Protected Attributes inherited from string_builtin_functiont
array_poolt &	array_pool

Detailed Description

String inserting a string into another one.

Definition at line 15 of file string_insertion_builtin_function.h.

Constructor & Destructor Documentation

◆ string_insertion_builtin_functiont() [1/2]

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.

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, and potentially some arguments of primitive types.

Definition at line 23 of file string_insertion_builtin_function.cpp.

◆ string_insertion_builtin_functiont() [2/2]

string_insertion_builtin_functiont::string_insertion_builtin_functiont	(	const exprt &	return_code,
		array_poolt &	array_pool
	)

inlineprotected

Definition at line 84 of file string_insertion_builtin_function.h.

Member Function Documentation

◆ constraints()

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

overridevirtual

Constraints ensuring the result corresponds to input1 where we inserted input2 at position offset given by the first argument.

We write offset' for max(0, min(input1.length, offset)). These axioms are:

result.length = input1.length + input2.length
forall i < offset' . result[i] = input1[i]
forall i < input2.length. res[i + offset'] = input2[i]
forall i in [offset', input1.length). res[i + input2.length] = input1[i] This is equivalent to ‘res=concat(substring(input1, 0, offset’), concat(input2, substring(input1, offset')))`.

Implements string_builtin_functiont.

Definition at line 89 of file string_insertion_builtin_function.cpp.

◆ eval() [1/2]

std::optional< exprt > string_insertion_builtin_functiont::eval ( const std::function< exprt(const exprt &)> & get_value ) const

overridevirtual

Given a function get_value which gives a valuation to expressions, attempt to find the result of the builtin function.

If not enough information can be gathered from get_value, return an empty optional.

Implements string_builtin_functiont.

Definition at line 65 of file string_insertion_builtin_function.cpp.

◆ eval() [2/2]

std::vector< mp_integer > string_insertion_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

virtual

Evaluate the result from a concrete valuation of the arguments.

Reimplemented in string_concatenation_builtin_functiont.

Definition at line 39 of file string_insertion_builtin_function.cpp.

◆ length_constraint()

exprt string_insertion_builtin_functiont::length_constraint ( ) const

overridevirtual

Returns: a constraint ensuring the length of result corresponds to that of input1 where we inserted input2. That is: result.length = input1.length + input2.length

Implements string_builtin_functiont.

Definition at line 13 of file string_insertion_builtin_function.cpp.

◆ maybe_testing_function()

bool string_insertion_builtin_functiont::maybe_testing_function ( ) const

inlineoverridevirtual

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.

Reimplemented from string_builtin_functiont.

Definition at line 78 of file string_insertion_builtin_function.h.