Converting each uppercase character of Basic Latin and Latin-1 supplement to the corresponding lowercase character. More...

#include <string_builtin_function.h>

Inheritance diagram for string_to_lower_case_builtin_functiont:

Collaboration diagram for string_to_lower_case_builtin_functiont:

Public Member Functions
	string_to_lower_case_builtin_functiont (const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)

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
	Set of constraints ensuring `result` corresponds to `input` in which uppercase characters have been converted to lowercase. 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

Additional Inherited Members
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

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

Converting each uppercase character of Basic Latin and Latin-1 supplement to the corresponding lowercase character.

Definition at line 249 of file string_builtin_function.h.

Constructor & Destructor Documentation

◆ string_to_lower_case_builtin_functiont()

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

inline

Definition at line 253 of file string_builtin_function.h.

Member Function Documentation

◆ constraints()

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

overridevirtual

Set of constraints ensuring result corresponds to input in which uppercase characters have been converted to lowercase.

These constraints are:

result.length = input.length && return_code = 0
forall i < input.length. result[i] = is_upper_case(input[i]) ? input[i] + diff : input[i]

Where diff is the difference between lower case and upper case characters: ‘diff = 'a’-'A' = 0x20andis_upper_case` is true for the upper case characters of Basic Latin and Latin-1 supplement of unicode.

Implements string_builtin_functiont.

Definition at line 285 of file string_builtin_function.cpp.