cprover
|
String creation from other types. More...
#include <string_builtin_function.h>
Public Member Functions | |
optionalt< 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... | |
![]() | |
string_builtin_functiont (const string_builtin_functiont &)=delete | |
virtual | ~string_builtin_functiont ()=default |
virtual std::vector< array_string_exprt > | string_arguments () const |
virtual optionalt< exprt > | eval (const std::function< exprt(const exprt &)> &get_value) const =0 |
virtual std::string | name () const =0 |
virtual exprt | add_constraints (string_constraint_generatort &constraint_generator) 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 |
std::vector< exprt > | args |
exprt | return_code |
![]() | |
exprt | return_code |
Additional Inherited Members | |
![]() | |
string_builtin_functiont (const exprt &return_code) | |
String creation from other types.
Definition at line 263 of file string_builtin_function.h.
|
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 275 of file string_builtin_function.h.
|
inlineoverridevirtual |
Reimplemented from string_builtin_functiont.
Definition at line 270 of file string_builtin_function.h.
References result.
std::vector<exprt> string_creation_builtin_functiont::args |
Definition at line 267 of file string_builtin_function.h.
array_string_exprt string_creation_builtin_functiont::result |
Definition at line 266 of file string_builtin_function.h.
Referenced by string_result().
exprt string_creation_builtin_functiont::return_code |
Definition at line 268 of file string_builtin_function.h.