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 |
| std::optional< array_string_exprt > | string_result () const override |
| std::optional< 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, message_handlert &message_handler) 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 ()=delete | |
| 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 |
| std::optional< 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, array_poolt &array_pool) | |
| Protected Attributes inherited from string_builtin_functiont | |
| array_poolt & | array_pool |
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 414 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 457 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.
The constraints are only added when deemed necessary, i.e. when maybe_testing_function() returns true, or when testing function depends on the result of this function. This logic is implemented in add_constraints().
Implements string_builtin_functiont.
Definition at line 487 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 443 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 452 of file string_builtin_function.h.
◆ name()
|
inlineoverridevirtual |
Implements string_builtin_functiont.
Definition at line 427 of file string_builtin_function.h.
◆ string_arguments()
|
inlineoverridevirtual |
Reimplemented from string_builtin_functiont.
Definition at line 433 of file string_builtin_function.h.
◆ string_result()
|
inlineoverridevirtual |
Reimplemented from string_builtin_functiont.
Definition at line 437 of file string_builtin_function.h.
Member Data Documentation
◆ args
| std::vector<exprt> string_builtin_function_with_no_evalt::args |
Definition at line 420 of file string_builtin_function.h.
◆ function_application
| function_application_exprt string_builtin_function_with_no_evalt::function_application |
Definition at line 417 of file string_builtin_function.h.
◆ string_args
| std::vector<array_string_exprt> string_builtin_function_with_no_evalt::string_args |
Definition at line 419 of file string_builtin_function.h.
◆ string_res
| std::optional<array_string_exprt> string_builtin_function_with_no_evalt::string_res |
Definition at line 418 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
