cprover
string_creation_builtin_functiont Class Reference

String creation from other types. More...

#include <string_builtin_function.h>

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

Public Member Functions

optionalt< array_string_exprtstring_result () 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
 
virtual std::vector< array_string_exprtstring_arguments () const
 
virtual optionalt< exprteval (const std::function< exprt(const exprt &)> &get_value) const =0
 
virtual std::string name () const =0
 
virtual exprt add_constraints (string_constraint_generatort &constraint_generator) const =0
 Add constraints ensuring that the value of result expression of the builtin function corresponds to the value of the function call. More...
 
virtual exprt length_constraint () const =0
 Constraint ensuring that the length of the strings are coherent with the function call. More...
 

Public Attributes

array_string_exprt result
 
std::vector< exprtargs
 
exprt return_code
 
- Public Attributes inherited from string_builtin_functiont
exprt return_code
 

Additional Inherited Members

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

Detailed Description

String creation from other types.

Definition at line 263 of file string_builtin_function.h.

Member Function Documentation

◆ maybe_testing_function()

bool string_creation_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 275 of file string_builtin_function.h.

◆ string_result()

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

Reimplemented from string_builtin_functiont.

Definition at line 270 of file string_builtin_function.h.

References result.

Member Data Documentation

◆ args

std::vector<exprt> string_creation_builtin_functiont::args

Definition at line 267 of file string_builtin_function.h.

◆ result

array_string_exprt string_creation_builtin_functiont::result

Definition at line 266 of file string_builtin_function.h.

Referenced by string_result().

◆ return_code

exprt string_creation_builtin_functiont::return_code

Definition at line 268 of file string_builtin_function.h.


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