Loading...

Searching...

No Matches

Public Member Functions | Public Attributes | List of all members

string_concat_char_builtin_functiont Class Reference

Adding a character at the end of a string. More...

#include <string_builtin_function.h>

+ Inheritance diagram for string_concat_char_builtin_functiont:

[フレーム]

[legend]

+ Collaboration diagram for string_concat_char_builtin_functiont:

[フレーム]

[legend]

Public Member Functions

string_concat_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_handlert) const override

Set of constraints enforcing that result is the concatenation of input with 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 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

Adding a character at the end of a string.

Definition at line 172 of file string_builtin_function.h.

Constructor & Destructor Documentation

◆ string_concat_char_builtin_functiont()

string_concat_char_builtin_functiont::string_concat_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, and a character.

Definition at line 182 of file string_builtin_function.h.

Member Function Documentation

◆ constraints()

string_constraintst string_concat_char_builtin_functiont::constraints ( string_constraint_generatort & generator,

message_handlert & message_handler

) const

overridevirtual

Set of constraints enforcing that result is the concatenation of input with character.

These constraints are :

result.length = input.length + 1
forall i < max(0, result.length). result[i] = input[i]
result[input.length] = character
return_code = 0

Implements string_builtin_functiont.

Definition at line 103 of file string_builtin_function.cpp.

◆ eval()

std::optional< exprt > string_concat_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 76 of file string_builtin_function.cpp.

◆ length_constraint()

exprt string_concat_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 124 of file string_builtin_function.cpp.

◆ name()

std::string string_concat_char_builtin_functiont::name ( ) const

inlineoverridevirtual

Implements string_builtin_functiont.

Definition at line 195 of file string_builtin_function.h.

Member Data Documentation

◆ character

exprt string_concat_char_builtin_functiont::character

Definition at line 176 of file string_builtin_function.h.

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

/home/runner/work/cbmc/cbmc/src/solvers/strings/string_builtin_function.h
/home/runner/work/cbmc/cbmc/src/solvers/strings/string_builtin_function.cpp