String inserting a string into another one. More...
#include <string_insertion_builtin_function.h>
Inheritance diagram for string_insertion_builtin_functiont: Collaboration diagram for string_insertion_builtin_functiont: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 |
Given a function get_value which gives a valuation to expressions, attempt to find the result of the builtin function. More... | |
| std::string | name () const override |
| string_constraintst | constraints (string_constraint_generatort &generator, message_handlert &message_handler) const override |
Constraints ensuring the result corresponds to input1 where we inserted input2 at position offset given by the first argument. More... | |
| exprt | length_constraint () 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... | |
| 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 |
Public Attributes | |
| array_string_exprt | result |
| array_string_exprt | input1 |
| array_string_exprt | input2 |
| std::vector< exprt > | args |
| Public Attributes inherited from string_builtin_functiont | |
| exprt | return_code |
Protected Member Functions | |
| string_insertion_builtin_functiont (const exprt &return_code, array_poolt &array_pool) | |
| Protected Member Functions inherited from string_builtin_functiont | |
| string_builtin_functiont (exprt return_code, array_poolt &array_pool) | |
Additional Inherited Members | |
| Protected Attributes inherited from string_builtin_functiont | |
| array_poolt & | array_pool |
Detailed Description
String inserting a string into another one.
Definition at line 15 of file string_insertion_builtin_function.h.
Constructor & Destructor Documentation
◆ string_insertion_builtin_functiont() [1/2]
| 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 23 of file string_insertion_builtin_function.cpp.
◆ string_insertion_builtin_functiont() [2/2]
|
inlineprotected |
Definition at line 84 of file string_insertion_builtin_function.h.
Member Function Documentation
◆ constraints()
|
overridevirtual |
Constraints ensuring the result corresponds to input1 where we inserted input2 at position offset given by the first argument.
We write offset' for max(0, min(input1.length, offset)). These axioms are:
- result.length = input1.length + input2.length
- forall i < offset' . result[i] = input1[i]
- forall i < input2.length. res[i + offset'] = input2[i]
- forall i in [offset', input1.length). res[i + input2.length] = input1[i] This is equivalent to ‘res=concat(substring(input1, 0, offset’), concat(input2, substring(input1, offset')))`.
Implements string_builtin_functiont.
Definition at line 89 of file string_insertion_builtin_function.cpp.
◆ eval() [1/2]
|
overridevirtual |
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 65 of file string_insertion_builtin_function.cpp.
◆ eval() [2/2]
|
virtual |
Evaluate the result from a concrete valuation of the arguments.
Reimplemented in string_concatenation_builtin_functiont.
Definition at line 39 of file string_insertion_builtin_function.cpp.
◆ length_constraint()
|
overridevirtual |
- Returns
- a constraint ensuring the length of
resultcorresponds to that ofinput1where we insertedinput2. That is:result.length = input1.length + input2.length
Implements string_builtin_functiont.
Definition at line 13 of file string_insertion_builtin_function.cpp.
◆ maybe_testing_function()
|
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 78 of file string_insertion_builtin_function.h.
◆ name()
|
inlineoverridevirtual |
Implements string_builtin_functiont.
Definition at line 52 of file string_insertion_builtin_function.h.
◆ string_arguments()
|
inlineoverridevirtual |
Reimplemented from string_builtin_functiont.
Definition at line 38 of file string_insertion_builtin_function.h.
◆ string_result()
|
inlineoverridevirtual |
Reimplemented from string_builtin_functiont.
Definition at line 34 of file string_insertion_builtin_function.h.
Member Data Documentation
◆ args
| std::vector<exprt> string_insertion_builtin_functiont::args |
Definition at line 21 of file string_insertion_builtin_function.h.
◆ input1
| array_string_exprt string_insertion_builtin_functiont::input1 |
Definition at line 19 of file string_insertion_builtin_function.h.
◆ input2
| array_string_exprt string_insertion_builtin_functiont::input2 |
Definition at line 20 of file string_insertion_builtin_function.h.
◆ result
| array_string_exprt string_insertion_builtin_functiont::result |
Definition at line 18 of file string_insertion_builtin_function.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc-documentation/cbmc-documentation/src/solvers/strings/string_insertion_builtin_function.h
- /home/runner/work/cbmc-documentation/cbmc-documentation/src/solvers/strings/string_insertion_builtin_function.cpp
