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) | |
| optionalt< 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... | |
| optionalt< 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 250 of file string_builtin_function.h.
Constructor & Destructor Documentation
◆ string_to_lower_case_builtin_functiont()
|
inline |
Definition at line 254 of file string_builtin_function.h.
Member Function Documentation
◆ constraints()
|
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.
◆ eval()
|
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 220 of file string_builtin_function.cpp.
◆ length_constraint()
|
inlineoverridevirtual |
Constraint ensuring that the length of the strings are coherent with the function call.
Implements string_builtin_functiont.
Definition at line 274 of file string_builtin_function.h.
◆ name()
|
inlineoverridevirtual |
Implements string_builtin_functiont.
Definition at line 265 of file string_builtin_function.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc-documentation/cbmc-documentation/src/solvers/strings/string_builtin_function.h
- /home/runner/work/cbmc-documentation/cbmc-documentation/src/solvers/strings/string_builtin_function.cpp
