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.

- 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]

string_insertion_builtin_functiont::string_insertion_builtin_functiont ( const exprt & return_code,

array_poolt & array_pool

)

inlineprotected

Definition at line 84 of file string_insertion_builtin_function.h.

Member Function Documentation

◆ constraints()

string_constraintst string_insertion_builtin_functiont::constraints ( string_constraint_generatort & generator,

message_handlert & message_handler

) const

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]

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

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]

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 39 of file string_insertion_builtin_function.cpp.

◆ length_constraint()

exprt string_insertion_builtin_functiont::length_constraint ( ) const

overridevirtual

Returns: a constraint ensuring the length of result corresponds to that of input1 where we inserted input2. 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()

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 78 of file string_insertion_builtin_function.h.