cprover
|
Converting each uppercase character of Basic Latin and Latin-1 supplement to the corresponding lowercase character. More...
#include <string_builtin_function.h>
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 |
exprt | add_constraints (string_constraint_generatort &generator) 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... | |
![]() | |
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... | |
![]() | |
string_builtin_functiont (const string_builtin_functiont &)=delete | |
virtual | ~string_builtin_functiont ()=default |
Additional Inherited Members | |
![]() | |
array_string_exprt | result |
array_string_exprt | input |
![]() | |
exprt | return_code |
![]() | |
string_builtin_functiont (const exprt &return_code) | |
Converting each uppercase character of Basic Latin and Latin-1 supplement to the corresponding lowercase character.
Definition at line 186 of file string_builtin_function.h.
|
inline |
Definition at line 190 of file string_builtin_function.h.
|
inlineoverridevirtual |
Add constraints ensuring that the value of result expression of the builtin function corresponds to the value of the function call.
Implements string_builtin_functiont.
Definition at line 206 of file string_builtin_function.h.
References string_constraint_generatort::add_axioms_for_to_lower_case(), string_transformation_builtin_functiont::input, and string_transformation_builtin_functiont::result.
|
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 203 of file string_builtin_function.cpp.
References eval_is_upper_case(), eval_string(), from_integer(), string_transformation_builtin_functiont::input, array_string_exprt::length(), make_string(), string_transformation_builtin_functiont::result, typet::subtype(), and exprt::type().
|
inlineoverridevirtual |
Constraint ensuring that the length of the strings are coherent with the function call.
Implements string_builtin_functiont.
Definition at line 211 of file string_builtin_function.h.
References string_transformation_builtin_functiont::input, array_string_exprt::length(), and string_transformation_builtin_functiont::result.
|
inlineoverridevirtual |
Implements string_builtin_functiont.
Definition at line 201 of file string_builtin_function.h.