String test. More...

Inheritance diagram for string_test_builtin_functiont:

Collaboration diagram for string_test_builtin_functiont:

Public Member Functions
std::vector< array_string_exprt >	string_arguments () const override

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< array_string_exprt >	string_result () const

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. More...

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. More...

virtual exprt	length_constraint () const =0
	Constraint ensuring that the length of the strings are coherent with the function call. More...

virtual bool	maybe_testing_function () const
	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 Attributes
exprt	result

std::vector< array_string_exprt >	under_test

std::vector< exprt >	args

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 test.

Definition at line 398 of file string_builtin_function.h.

Member Function Documentation

std::vector<array_string_exprt> string_test_builtin_functiont::string_arguments ( ) const

inlineoverridevirtual

Definition at line 404 of file string_builtin_function.h.

std::vector<exprt> string_test_builtin_functiont::args

Definition at line 403 of file string_builtin_function.h.

exprt string_test_builtin_functiont::result

Definition at line 401 of file string_builtin_function.h.

std::vector<array_string_exprt> string_test_builtin_functiont::under_test

Definition at line 402 of file string_builtin_function.h.

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