Functions that are not yet supported in this class but are supported by string_constraint_generatort. More...
#include <string_builtin_function.h>
Inheritance diagram for string_builtin_function_with_no_evalt: Collaboration diagram for string_builtin_function_with_no_evalt:Public Member Functions | |
| string_builtin_function_with_no_evalt (const exprt &return_code, const function_application_exprt &f, array_poolt &array_pool) | |
| std::string | name () const override |
| std::vector< array_string_exprt > | string_arguments () const override |
| optionalt< array_string_exprt > | string_result () const override |
| optionalt< exprt > | eval (const std::function< exprt(const exprt &)> &) const override |
Given a function get_value which gives a valuation to expressions, attempt to find the result of the builtin function. More... | |
| string_constraintst | 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... | |
| Public Member Functions inherited from string_builtin_functiont | |
| string_builtin_functiont (const string_builtin_functiont &)=delete | |
| virtual | ~string_builtin_functiont ()=default |
| virtual bool | maybe_testing_function () const |
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 Attributes | |
| function_application_exprt | function_application |
| optionalt< array_string_exprt > | string_res |
| std::vector< array_string_exprt > | string_args |
| std::vector< exprt > | args |
| 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) | |
Detailed Description
Functions that are not yet supported in this class but are supported by string_constraint_generatort.
- Note
- Ultimately this should be disappear, once all builtin function have a corresponding string_builtin_functiont class.
Definition at line 435 of file string_builtin_function.h.
Constructor & Destructor Documentation
◆ string_builtin_function_with_no_evalt()
| string_builtin_function_with_no_evalt::string_builtin_function_with_no_evalt | ( | const exprt & | return_code, |
| const function_application_exprt & | f, | ||
| array_poolt & | array_pool | ||
| ) |
Definition at line 604 of file string_builtin_function.cpp.
Member Function Documentation
◆ constraints()
|
overridevirtual |
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 634 of file string_builtin_function.cpp.
◆ eval()
|
inlineoverridevirtual |
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 462 of file string_builtin_function.h.
◆ length_constraint()
|
inlineoverridevirtual |
Constraint ensuring that the length of the strings are coherent with the function call.
Implements string_builtin_functiont.
Definition at line 470 of file string_builtin_function.h.
◆ name()
|
inlineoverridevirtual |
Implements string_builtin_functiont.
Definition at line 448 of file string_builtin_function.h.
◆ string_arguments()
|
inlineoverridevirtual |
Reimplemented from string_builtin_functiont.
Definition at line 452 of file string_builtin_function.h.
◆ string_result()
|
inlineoverridevirtual |
Reimplemented from string_builtin_functiont.
Definition at line 456 of file string_builtin_function.h.
Member Data Documentation
◆ args
| std::vector<exprt> string_builtin_function_with_no_evalt::args |
Definition at line 441 of file string_builtin_function.h.
◆ function_application
| function_application_exprt string_builtin_function_with_no_evalt::function_application |
Definition at line 438 of file string_builtin_function.h.
◆ string_args
| std::vector<array_string_exprt> string_builtin_function_with_no_evalt::string_args |
Definition at line 440 of file string_builtin_function.h.
◆ string_res
| optionalt<array_string_exprt> string_builtin_function_with_no_evalt::string_res |
Definition at line 439 of file string_builtin_function.h.
The documentation for this class was generated from the following files:
- solvers/refinement/string_builtin_function.h
- solvers/refinement/string_builtin_function.cpp
