Converting each lowercase character of Basic Latin and Latin-1 supplement to the corresponding uppercase character. More...
#include <string_builtin_function.h>
Inheritance diagram for string_to_upper_case_builtin_functiont: Collaboration diagram for string_to_upper_case_builtin_functiont:Public Member Functions | |
| string_to_upper_case_builtin_functiont (const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool) | |
| string_to_upper_case_builtin_functiont (exprt return_code, array_string_exprt result, array_string_exprt input, 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 (class symbol_generatort &fresh_symbol, message_handlert &message_handler) const |
Set of constraints ensuring result corresponds to input in which lowercase characters of Basic Latin and Latin-1 supplement of unicode have been converted to uppercase. More... | |
| 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_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 lowercase character of Basic Latin and Latin-1 supplement to the corresponding uppercase character.
Definition at line 285 of file string_builtin_function.h.
Constructor & Destructor Documentation
◆ string_to_upper_case_builtin_functiont() [1/2]
|
inline |
Definition at line 289 of file string_builtin_function.h.
◆ string_to_upper_case_builtin_functiont() [2/2]
|
inline |
Definition at line 297 of file string_builtin_function.h.
Member Function Documentation
◆ constraints() [1/2]
| string_constraintst string_to_upper_case_builtin_functiont::constraints | ( | class symbol_generatort & | fresh_symbol, |
| message_handlert & | message_handler | ||
| ) | const |
Set of constraints ensuring result corresponds to input in which lowercase characters of Basic Latin and Latin-1 supplement of unicode have been converted to uppercase.
These constraints are:
- res.length = str.length && return_code = 0
- forall i < str.length. is_lower_case(str[i]) ? res[i] = str[i] - 0x20 : res[i] = str[i]
- Parameters
-
fresh_symbol generator of fresh symbols message_handler message handler
- Returns
- set of constraints
Definition at line 343 of file string_builtin_function.cpp.
◆ constraints() [2/2]
|
inlineoverridevirtual |
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 322 of file string_builtin_function.h.
◆ 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 316 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 329 of file string_builtin_function.h.
◆ name()
|
inlineoverridevirtual |
Implements string_builtin_functiont.
Definition at line 313 of file string_builtin_function.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/solvers/strings/string_builtin_function.h
- /home/runner/work/cbmc/cbmc/src/solvers/strings/string_builtin_function.cpp
