cprover
|
Functions that are not yet supported in this class but are supported by string_constraint_generatort. More...
#include <string_builtin_function.h>
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... | |
![]() | |
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 |
![]() | |
exprt | return_code |
Additional Inherited Members | |
![]() | |
string_builtin_functiont (exprt return_code) | |
Functions that are not yet supported in this class but are supported by string_constraint_generatort.
Definition at line 435 of file string_builtin_function.h.
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.
|
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.
|
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.
|
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.
|
inlineoverridevirtual |
Implements string_builtin_functiont.
Definition at line 448 of file string_builtin_function.h.
|
inlineoverridevirtual |
Reimplemented from string_builtin_functiont.
Definition at line 452 of file string_builtin_function.h.
|
inlineoverridevirtual |
Reimplemented from string_builtin_functiont.
Definition at line 456 of file string_builtin_function.h.
std::vector<exprt> string_builtin_function_with_no_evalt::args |
Definition at line 441 of file string_builtin_function.h.
function_application_exprt string_builtin_function_with_no_evalt::function_application |
Definition at line 438 of file string_builtin_function.h.
std::vector<array_string_exprt> string_builtin_function_with_no_evalt::string_args |
Definition at line 440 of file string_builtin_function.h.
optionalt<array_string_exprt> string_builtin_function_with_no_evalt::string_res |
Definition at line 439 of file string_builtin_function.h.