CBMC
Public Member Functions | Public Attributes | List of all members
string_test_builtin_functiont Class Reference

String test. More...

#include <string_builtin_function.h>

+ 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 optionalt< array_string_exprt > string_result () const
 
virtual optionalt< 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 399 of file string_builtin_function.h.

Member Function Documentation

◆ string_arguments()

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

Reimplemented from string_builtin_functiont.

Definition at line 405 of file string_builtin_function.h.

Member Data Documentation

◆ args

std::vector<exprt> string_test_builtin_functiont::args

Definition at line 404 of file string_builtin_function.h.

◆ result

exprt string_test_builtin_functiont::result

Definition at line 402 of file string_builtin_function.h.

◆ under_test

std::vector<array_string_exprt> string_test_builtin_functiont::under_test

Definition at line 403 of file string_builtin_function.h.

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