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< exprt > eval (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_poolt & array_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:

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