cprover
|
String inserting a string into another one. More...
#include <string_builtin_function.h>
Public Member Functions | |
string_insertion_builtin_functiont (const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool) | |
Constructor from arguments of a function application. More... | |
optionalt< array_string_exprt > | string_result () const override |
std::vector< array_string_exprt > | string_arguments () const override |
virtual std::vector< mp_integer > | eval (const std::vector< mp_integer > &input1_value, const std::vector< mp_integer > &input2_value, const std::vector< mp_integer > &args_value) const |
Evaluate the result from a concrete valuation of the arguments. More... | |
optionalt< exprt > | eval (const std::function< exprt(const exprt &)> &get_value) const override |
std::string | name () const override |
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... | |
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 |
Public Attributes | |
array_string_exprt | result |
array_string_exprt | input1 |
array_string_exprt | input2 |
std::vector< exprt > | args |
![]() | |
exprt | return_code |
Protected Member Functions | |
string_insertion_builtin_functiont (const exprt &return_code) | |
![]() | |
string_builtin_functiont (const exprt &return_code) | |
String inserting a string into another one.
Definition at line 144 of file string_builtin_function.h.
string_insertion_builtin_functiont::string_insertion_builtin_functiont | ( | const exprt & | return_code, |
const std::vector< exprt > & | fun_args, | ||
array_poolt & | array_pool | ||
) |
Constructor from arguments of a function application.
The arguments in fun_args
should be in order: an integer result.length
, a character pointer &result[0]
, a string arg1
of type refined_string_typet, a string arg2
of type refined_string_typet, and potentially some arguments of primitive types.
Definition at line 61 of file string_builtin_function.cpp.
References args, expr_checked_cast(), array_poolt::find(), input1, input2, PRECONDITION, and result.
|
inlineexplicitprotected |
Definition at line 210 of file string_builtin_function.h.
|
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.
Reimplemented in string_concatenation_builtin_functiont.
Definition at line 186 of file string_builtin_function.h.
References string_constraint_generatort::add_axioms_for_insert(), args, input1, input2, result, UNIMPLEMENTED, and UNREACHABLE.
|
virtual |
Evaluate the result from a concrete valuation of the arguments.
Reimplemented in string_concatenation_builtin_functiont.
Definition at line 169 of file string_builtin_function.cpp.
References PRECONDITION, and result.
Referenced by eval().
|
overridevirtual |
Implements string_builtin_functiont.
Definition at line 195 of file string_builtin_function.cpp.
References args, eval(), eval_string(), from_integer(), input1, input2, array_string_exprt::length(), make_string(), result, typet::subtype(), and exprt::type().
|
inlineoverridevirtual |
Constraint ensuring that the length of the strings are coherent with the function call.
Implements string_builtin_functiont.
Reimplemented in string_concatenation_builtin_functiont.
Definition at line 195 of file string_builtin_function.h.
References args, input1, input2, length_constraint_for_insert(), result, UNIMPLEMENTED, and UNREACHABLE.
|
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 204 of file string_builtin_function.h.
|
inlineoverridevirtual |
Implements string_builtin_functiont.
Reimplemented in string_concatenation_builtin_functiont.
Definition at line 181 of file string_builtin_function.h.
|
inlineoverridevirtual |
Reimplemented from string_builtin_functiont.
Definition at line 167 of file string_builtin_function.h.
|
inlineoverridevirtual |
Reimplemented from string_builtin_functiont.
Definition at line 163 of file string_builtin_function.h.
References result.
std::vector<exprt> string_insertion_builtin_functiont::args |
Definition at line 150 of file string_builtin_function.h.
Referenced by add_constraints(), string_concatenation_builtin_functiont::add_constraints(), eval(), length_constraint(), string_concatenation_builtin_functiont::length_constraint(), string_concatenation_builtin_functiont::string_concatenation_builtin_functiont(), and string_insertion_builtin_functiont().
array_string_exprt string_insertion_builtin_functiont::input1 |
Definition at line 148 of file string_builtin_function.h.
Referenced by add_constraints(), string_concatenation_builtin_functiont::add_constraints(), eval(), length_constraint(), string_concatenation_builtin_functiont::length_constraint(), string_arguments(), string_concatenation_builtin_functiont::string_concatenation_builtin_functiont(), and string_insertion_builtin_functiont().
array_string_exprt string_insertion_builtin_functiont::input2 |
Definition at line 149 of file string_builtin_function.h.
Referenced by add_constraints(), string_concatenation_builtin_functiont::add_constraints(), eval(), length_constraint(), string_concatenation_builtin_functiont::length_constraint(), string_arguments(), string_concatenation_builtin_functiont::string_concatenation_builtin_functiont(), and string_insertion_builtin_functiont().
array_string_exprt string_insertion_builtin_functiont::result |
Definition at line 147 of file string_builtin_function.h.
Referenced by add_constraints(), string_concatenation_builtin_functiont::add_constraints(), eval(), string_concatenation_builtin_functiont::eval(), length_constraint(), string_concatenation_builtin_functiont::length_constraint(), string_concatenation_builtin_functiont::string_concatenation_builtin_functiont(), string_insertion_builtin_functiont(), and string_result().