cprover
|
Setting a character at a particular position of a string. More...
#include <string_builtin_function.h>
Public Member Functions | |
string_set_char_builtin_functiont (const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool) | |
Constructor from arguments of a function application. | |
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. | |
std::string | name () const override |
string_constraintst | constraints (string_constraint_generatort &generator, message_handlert &message_handler) const override |
Set of constraints ensuring that result is similar to input where the character at index position is set to character. | |
exprt | length_constraint () const override |
Constraint ensuring that the length of the strings are coherent with the function call. | |
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. | |
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. | |
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 | |
exprt | position |
exprt | character |
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 |
Additional Inherited Members | |
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 |
Setting a character at a particular position of a string.
Definition at line 208 of file string_builtin_function.h.
|
inline |
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 position and a character.
Definition at line 219 of file string_builtin_function.h.
|
overridevirtual |
Set of constraints ensuring that result is similar to input where the character at index position is set to character.
If position is out of bounds, input and result are identical. These constraints are:
Implements string_builtin_functiont.
Definition at line 154 of file string_builtin_function.cpp.
|
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 129 of file string_builtin_function.cpp.
|
overridevirtual |
Constraint ensuring that the length of the strings are coherent with the function call.
Implements string_builtin_functiont.
Definition at line 191 of file string_builtin_function.cpp.
|
inlineoverridevirtual |
Implements string_builtin_functiont.
Definition at line 233 of file string_builtin_function.h.
exprt string_set_char_builtin_functiont::character |
Definition at line 213 of file string_builtin_function.h.
exprt string_set_char_builtin_functiont::position |
Definition at line 212 of file string_builtin_function.h.