cprover
Loading...
Searching...
No Matches
string_transformation_builtin_functiont Class Reference

String builtin_function transforming one string into another. More...

#include <string_builtin_function.h>

Inheritance diagram for string_transformation_builtin_functiont:
Collaboration diagram for string_transformation_builtin_functiont:

Public Member Functions

 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_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.
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
virtual std::optional< exprteval (const std::function< exprt(const exprt &)> &get_value) const =0
 Given a function get_value which gives a valuation to expressions, attempt to find the result of the builtin function.
virtual std::string name () const =0
virtual string_constraintst constraints (string_constraint_generatort &, message_handlert &) const =0
 Add constraints ensuring that the value of result expression of the builtin function corresponds to the value of the function call.
virtual exprt length_constraint () const =0
 Constraint ensuring that the length of the strings are coherent with the function call.

Public Attributes

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_pooltarray_pool

Detailed Description

String builtin_function transforming one string into another.

Definition at line 130 of file string_builtin_function.h.

Constructor & Destructor Documentation

◆ string_transformation_builtin_functiont() [1/2]

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

Definition at line 136 of file string_builtin_function.h.

◆ string_transformation_builtin_functiont() [2/2]

string_transformation_builtin_functiont::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.

Module: String solver Author: Diffblue Ltd.

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 potentially some arguments of primitive types.

Definition at line 11 of file string_builtin_function.cpp.

Member Function Documentation

◆ maybe_testing_function()

bool string_transformation_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 165 of file string_builtin_function.h.

◆ string_arguments()

std::vector< array_string_exprt > string_transformation_builtin_functiont::string_arguments ( ) const
inlineoverridevirtual

Reimplemented from string_builtin_functiont.

Definition at line 161 of file string_builtin_function.h.

◆ string_result()

std::optional< array_string_exprt > string_transformation_builtin_functiont::string_result ( ) const
inlineoverridevirtual

Reimplemented from string_builtin_functiont.

Definition at line 157 of file string_builtin_function.h.

Member Data Documentation

◆ input

array_string_exprt string_transformation_builtin_functiont::input

Definition at line 134 of file string_builtin_function.h.

◆ result

array_string_exprt string_transformation_builtin_functiont::result

Definition at line 133 of file string_builtin_function.h.


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