cprover
string_builtin_function_with_no_evalt Class Reference

Functions that are not yet supported in this class but are supported by string_constraint_generatort. More...

#include <string_builtin_function.h>

+ Inheritance diagram for string_builtin_function_with_no_evalt:
+ Collaboration diagram for string_builtin_function_with_no_evalt:

Public Member Functions

 string_builtin_function_with_no_evalt (const exprt &return_code, const function_application_exprt &f, array_poolt &array_pool)
 
std::string name () const override
 
std::vector< array_string_exprtstring_arguments () const override
 
optionalt< array_string_exprtstring_result () const override
 
optionalt< exprteval (const std::function< exprt(const exprt &)> &) const override
 Given a function get_value which gives a valuation to expressions, attempt to find the result of the builtin function. More...
 
string_constraintst constraints (string_constraint_generatort &generator) const override
 Add constraints ensuring that the value of result expression of the builtin function corresponds to the value of the function call. More...
 
exprt length_constraint () const override
 Constraint ensuring that the length of the strings are coherent with the function call. More...
 
- Public Member Functions inherited from string_builtin_functiont
 string_builtin_functiont (const string_builtin_functiont &)=delete
 
virtual ~string_builtin_functiont ()=default
 
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

function_application_exprt function_application
 
optionalt< array_string_exprtstring_res
 
std::vector< array_string_exprtstring_args
 
std::vector< exprtargs
 
- 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)
 

Detailed Description

Functions that are not yet supported in this class but are supported by string_constraint_generatort.

Note
Ultimately this should be disappear, once all builtin function have a corresponding string_builtin_functiont class.

Definition at line 435 of file string_builtin_function.h.

Constructor & Destructor Documentation

◆ string_builtin_function_with_no_evalt()

string_builtin_function_with_no_evalt::string_builtin_function_with_no_evalt ( const exprt return_code,
const function_application_exprt f,
array_poolt array_pool 
)

Definition at line 604 of file string_builtin_function.cpp.

Member Function Documentation

◆ constraints()

string_constraintst string_builtin_function_with_no_evalt::constraints ( string_constraint_generatort constraint_generator) const
overridevirtual

Add constraints ensuring that the value of result expression of the builtin function corresponds to the value of the function call.

Implements string_builtin_functiont.

Definition at line 634 of file string_builtin_function.cpp.

◆ eval()

optionalt<exprt> string_builtin_function_with_no_evalt::eval ( const std::function< exprt(const exprt &)> &  get_value) const
inlineoverridevirtual

Given a function get_value which gives a valuation to expressions, attempt to find the result of the builtin function.

If not enough information can be gathered from get_value, return an empty optional.

Implements string_builtin_functiont.

Definition at line 462 of file string_builtin_function.h.

◆ length_constraint()

exprt string_builtin_function_with_no_evalt::length_constraint ( ) const
inlineoverridevirtual

Constraint ensuring that the length of the strings are coherent with the function call.

Implements string_builtin_functiont.

Definition at line 470 of file string_builtin_function.h.

◆ name()

std::string string_builtin_function_with_no_evalt::name ( ) const
inlineoverridevirtual

Implements string_builtin_functiont.

Definition at line 448 of file string_builtin_function.h.

◆ string_arguments()

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

Reimplemented from string_builtin_functiont.

Definition at line 452 of file string_builtin_function.h.

◆ string_result()

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

Reimplemented from string_builtin_functiont.

Definition at line 456 of file string_builtin_function.h.

Member Data Documentation

◆ args

std::vector<exprt> string_builtin_function_with_no_evalt::args

Definition at line 441 of file string_builtin_function.h.

◆ function_application

function_application_exprt string_builtin_function_with_no_evalt::function_application

Definition at line 438 of file string_builtin_function.h.

◆ string_args

std::vector<array_string_exprt> string_builtin_function_with_no_evalt::string_args

Definition at line 440 of file string_builtin_function.h.

◆ string_res

optionalt<array_string_exprt> string_builtin_function_with_no_evalt::string_res

Definition at line 439 of file string_builtin_function.h.


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