cprover
string_insertion_builtin_functiont Class Reference

String inserting a string into another one. More...

#include <string_builtin_function.h>

Inheritance diagram for string_insertion_builtin_functiont:
[legend]
Collaboration diagram for string_insertion_builtin_functiont:
[legend]

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_exprtstring_result () const override
 
std::vector< array_string_exprtstring_arguments () const override
 
virtual std::vector< mp_integereval (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< exprteval (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...
 
- Public Member Functions inherited from string_builtin_functiont
 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< exprtargs
 
- Public Attributes inherited from string_builtin_functiont
exprt return_code
 

Protected Member Functions

 string_insertion_builtin_functiont (const exprt &return_code)
 
- Protected Member Functions inherited from string_builtin_functiont
 string_builtin_functiont (const exprt &return_code)
 

Detailed Description

String inserting a string into another one.

Definition at line 144 of file string_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 61 of file string_builtin_function.cpp.

References args, expr_checked_cast(), array_poolt::find(), input1, input2, PRECONDITION, and result.

◆ string_insertion_builtin_functiont() [2/2]

string_insertion_builtin_functiont::string_insertion_builtin_functiont ( const exprt return_code)
inlineexplicitprotected

Definition at line 210 of file string_builtin_function.h.

Member Function Documentation

◆ add_constraints()

exprt string_insertion_builtin_functiont::add_constraints ( string_constraint_generatort constraint_generator) const
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.

◆ eval() [1/2]

std::vector< mp_integer > string_insertion_builtin_functiont::eval ( const std::vector< mp_integer > &  input1_value,
const std::vector< mp_integer > &  input2_value,
const std::vector< mp_integer > &  args_value 
) const
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().

◆ eval() [2/2]

optionalt< exprt > string_insertion_builtin_functiont::eval ( const std::function< exprt(const exprt &)> &  get_value) const
overridevirtual

◆ length_constraint()

exprt string_insertion_builtin_functiont::length_constraint ( ) const
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.

◆ maybe_testing_function()

bool string_insertion_builtin_functiont::maybe_testing_function ( ) const
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.

◆ name()

std::string string_insertion_builtin_functiont::name ( ) const
inlineoverridevirtual

Implements string_builtin_functiont.

Reimplemented in string_concatenation_builtin_functiont.

Definition at line 181 of file string_builtin_function.h.

◆ string_arguments()

std::vector<array_string_exprt> string_insertion_builtin_functiont::string_arguments ( ) const
inlineoverridevirtual

Reimplemented from string_builtin_functiont.

Definition at line 167 of file string_builtin_function.h.

References input1, and input2.

◆ string_result()

optionalt<array_string_exprt> string_insertion_builtin_functiont::string_result ( ) const
inlineoverridevirtual

Reimplemented from string_builtin_functiont.

Definition at line 163 of file string_builtin_function.h.

References result.

Member Data Documentation

◆ args

◆ input1

◆ input2

◆ result


The documentation for this class was generated from the following files: