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... | |
exprt | add_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 (const exprt &return_code) | |
Functions that are not yet supported in this class but are supported by string_constraint_generatort.
Definition at line 446 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 365 of file string_builtin_function.cpp.
References args, function_application_exprt::arguments(), expr_try_dynamic_cast(), array_poolt::find(), INVARIANT, is_refined_string_type(), string_args, and string_res.
|
inlineoverridevirtual |
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 478 of file string_builtin_function.h.
References string_constraint_generatort::add_axioms_for_function_application(), and function_application.
|
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 473 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 483 of file string_builtin_function.h.
References UNIMPLEMENTED.
|
inlineoverridevirtual |
Implements string_builtin_functiont.
Definition at line 459 of file string_builtin_function.h.
References function_application_exprt::function(), function_application, symbol_exprt::get_identifier(), and id2string().
|
inlineoverridevirtual |
Reimplemented from string_builtin_functiont.
Definition at line 463 of file string_builtin_function.h.
References string_args.
|
inlineoverridevirtual |
Reimplemented from string_builtin_functiont.
Definition at line 467 of file string_builtin_function.h.
References string_res.
std::vector<exprt> string_builtin_function_with_no_evalt::args |
Definition at line 452 of file string_builtin_function.h.
Referenced by string_builtin_function_with_no_evalt().
function_application_exprt string_builtin_function_with_no_evalt::function_application |
Definition at line 449 of file string_builtin_function.h.
Referenced by add_constraints(), and name().
std::vector<array_string_exprt> string_builtin_function_with_no_evalt::string_args |
Definition at line 451 of file string_builtin_function.h.
Referenced by string_arguments(), and string_builtin_function_with_no_evalt().
optionalt<array_string_exprt> string_builtin_function_with_no_evalt::string_res |
Definition at line 450 of file string_builtin_function.h.
Referenced by string_builtin_function_with_no_evalt(), and string_result().