String builtin_function transforming one string into another. More...
#include <string_builtin_function.h>
Inheritance diagram for string_transformation_builtin_functiont: Collaboration diagram for string_transformation_builtin_functiont:Public Member Functions | |
| 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 |
| virtual std::optional< exprt > | eval (const std::function< exprt(const exprt &)> &get_value) const =0 |
Given a function get_value which gives a valuation to expressions, attempt to find the result of the builtin function. More... | |
| virtual std::string | name () const =0 |
| virtual string_constraintst | constraints (string_constraint_generatort &, message_handlert &) const =0 |
| Add constraints ensuring that the value of result expression of the builtin function corresponds to the value of the function call. More... | |
| virtual exprt | length_constraint () const =0 |
| Constraint ensuring that the length of the strings are coherent with the function call. More... | |
Public Attributes | |
| 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 |
Detailed Description
String builtin_function transforming one string into another.
Definition at line 130 of file string_builtin_function.h.
Constructor & Destructor Documentation
◆ string_transformation_builtin_functiont() [1/2]
|
inline |
Definition at line 136 of file string_builtin_function.h.
◆ string_transformation_builtin_functiont() [2/2]
| string_transformation_builtin_functiont::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.
Module: String solver Author: Diffblue Ltd.
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, and potentially some arguments of primitive types.
Definition at line 11 of file string_builtin_function.cpp.
Member Function Documentation
◆ maybe_testing_function()
|
inlineoverridevirtual |
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.
Reimplemented from string_builtin_functiont.
Definition at line 165 of file string_builtin_function.h.
◆ string_arguments()
|
inlineoverridevirtual |
Reimplemented from string_builtin_functiont.
Definition at line 161 of file string_builtin_function.h.
◆ string_result()
|
inlineoverridevirtual |
Reimplemented from string_builtin_functiont.
Definition at line 157 of file string_builtin_function.h.
Member Data Documentation
◆ input
| array_string_exprt string_transformation_builtin_functiont::input |
Definition at line 134 of file string_builtin_function.h.
◆ result
| array_string_exprt string_transformation_builtin_functiont::result |
Definition at line 133 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
