cprover
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:
+ Collaboration diagram for string_set_char_builtin_functiont:

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. More...
 
optionalt< exprteval (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) const override
 Set of constraints ensuring that result is similar to input where the character at index position is set to character. More...
 
exprt length_constraint () const override
 Constraint ensuring that the length of the strings are coherent with the function call. More...
 
- Public Member Functions inherited from string_transformation_builtin_functiont
 string_transformation_builtin_functiont (exprt return_code, array_string_exprt result, array_string_exprt input)
 
 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. More...
 
optionalt< array_string_exprtstring_result () const override
 
std::vector< array_string_exprtstring_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. More...
 
- Public Member Functions inherited from string_builtin_functiont
 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)
 

Detailed Description

Setting a character at a particular position of a string.

Definition at line 150 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 161 of file string_builtin_function.h.

Member Function Documentation

◆ constraints()

string_constraintst string_set_char_builtin_functiont::constraints ( string_constraint_generatort generator) 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:

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

Implements string_builtin_functiont.

Definition at line 245 of file string_builtin_function.cpp.

◆ eval()

optionalt< exprt > string_set_char_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 220 of file string_builtin_function.cpp.

◆ length_constraint()

exprt string_set_char_builtin_functiont::length_constraint ( ) const
overridevirtual

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

Implements string_builtin_functiont.

Definition at line 275 of file string_builtin_function.cpp.

◆ name()

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

Implements string_builtin_functiont.

Definition at line 175 of file string_builtin_function.h.

Member Data Documentation

◆ character

exprt string_set_char_builtin_functiont::character

Definition at line 155 of file string_builtin_function.h.

◆ position

exprt string_set_char_builtin_functiont::position

Definition at line 154 of file string_builtin_function.h.


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