String creation from other types. More...
#include <string_builtin_function.h>
Inheritance diagram for string_creation_builtin_functiont: Collaboration diagram for string_creation_builtin_functiont:Public Member Functions | |
| string_creation_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 |
| 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::vector< array_string_exprt > | string_arguments () const |
| 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 |
| exprt | arg |
| 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 creation from other types.
Definition at line 340 of file string_builtin_function.h.
Constructor & Destructor Documentation
◆ string_creation_builtin_functiont()
| string_creation_builtin_functiont::string_creation_builtin_functiont | ( | const exprt & | return_code, |
| const std::vector< exprt > & | fun_args, | ||
| array_poolt & | array_pool | ||
| ) |
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], an expression arg which is to be converted to a string. Other arguments are ignored by this constructor.
Definition at line 372 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 356 of file string_builtin_function.h.
◆ string_result()
|
inlineoverridevirtual |
Reimplemented from string_builtin_functiont.
Definition at line 351 of file string_builtin_function.h.
Member Data Documentation
◆ arg
| exprt string_creation_builtin_functiont::arg |
Definition at line 344 of file string_builtin_function.h.
◆ result
| array_string_exprt string_creation_builtin_functiont::result |
Definition at line 343 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
