Loading...

Searching...

No Matches

Public Member Functions | Public Attributes | List of all members

string_set_char_builtin_functiont Class Reference

Setting a character at a particular position of a string. More...

#include <string_builtin_function.h>

+ Inheritance diagram for string_set_char_builtin_functiont:

[フレーム]

[legend]

+ Collaboration diagram for string_set_char_builtin_functiont:

[フレーム]

[legend]

Public Member Functions

string_set_char_builtin_functiont (const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)

Constructor from arguments of a function application.

std::optional< 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.

std::string name () const override

string_constraintst constraints (string_constraint_generatort &generator, message_handlert &message_handler) const override

Set of constraints ensuring that result is similar to input where the character at index position is set to character.

exprt length_constraint () const override

Constraint ensuring that the length of the strings are coherent with the function call.

- Public Member Functions inherited from string_transformation_builtin_functiont

string_transformation_builtin_functiont (exprt return_code, array_string_exprt result, array_string_exprt input, array_poolt &array_pool)

string_transformation_builtin_functiont (const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)

Constructor from arguments of a function application.

std::optional< array_string_exprt > string_result () const override

std::vector< array_string_exprt > string_arguments () 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.

- 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

exprt position

exprt character

- Public Attributes inherited from string_transformation_builtin_functiont

array_string_exprt result

array_string_exprt input

- Public Attributes inherited from string_builtin_functiont

exprt return_code

Additional Inherited Members

- Protected Member Functions inherited from string_builtin_functiont

string_builtin_functiont (exprt return_code, array_poolt &array_pool)

- Protected Attributes inherited from string_builtin_functiont

array_poolt & array_pool

Detailed Description

Setting a character at a particular position of a string.

Definition at line 208 of file string_builtin_function.h.

Constructor & Destructor Documentation

◆ string_set_char_builtin_functiont()

string_set_char_builtin_functiont::string_set_char_builtin_functiont ( const exprt & return_code,

const std::vector< exprt > & fun_args,

array_poolt & array_pool

)

inline

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 position and a character.

Definition at line 219 of file string_builtin_function.h.

Member Function Documentation

◆ constraints()

string_constraintst string_set_char_builtin_functiont::constraints ( string_constraint_generatort & generator,

message_handlert & message_handler

) const

overridevirtual

Set of constraints ensuring that result is similar to input where the character at index position is set to character.

If position is out of bounds, input and result are identical. These constraints are:

res.length = str.length && return_code = (position >= res.length || position < 0) ? 1 : 0
0 <= pos < res.length ==> res[pos]=char
forall 0 <= i < max(0, min(res.length, pos)). res[i] = str[i]
forall max(0, pos+1) <= i < res.length. res[i] = str[i]

Implements string_builtin_functiont.

Definition at line 154 of file string_builtin_function.cpp.