Loading...

Searching...

No Matches

Public Member Functions | Public Attributes | List of all members

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:

[フレーム]

[legend]

+ Collaboration diagram for string_builtin_function_with_no_evalt:

[フレーム]

[legend]

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_exprt > string_arguments () const override

std::optional< array_string_exprt > string_result () const override

std::optional< exprt > eval (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.

string_constraintst constraints (string_constraint_generatort &generator, message_handlert &message_handler) const override

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

exprt length_constraint () const override

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

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

Public Attributes

function_application_exprt function_application

std::optional< array_string_exprt > string_res

std::vector< array_string_exprt > string_args

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

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 414 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 457 of file string_builtin_function.cpp.

Member Function Documentation

◆ constraints()

string_constraintst string_builtin_function_with_no_evalt::constraints ( string_constraint_generatort & ,

message_handlert &

) const

overridevirtual

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

The constraints are only added when deemed necessary, i.e. when maybe_testing_function() returns true, or when testing function depends on the result of this function. This logic is implemented in add_constraints().

Implements string_builtin_functiont.

Definition at line 487 of file string_builtin_function.cpp.

◆ eval()

std::optional< 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 443 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 452 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 427 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 433 of file string_builtin_function.h.

◆ string_result()

std::optional< array_string_exprt > string_builtin_function_with_no_evalt::string_result ( ) const

inlineoverridevirtual

Reimplemented from string_builtin_functiont.

Definition at line 437 of file string_builtin_function.h.

Member Data Documentation

◆ args

std::vector<exprt> string_builtin_function_with_no_evalt::args

Definition at line 420 of file string_builtin_function.h.

◆ function_application

function_application_exprt string_builtin_function_with_no_evalt::function_application

Definition at line 417 of file string_builtin_function.h.

◆ string_args

std::vector<array_string_exprt> string_builtin_function_with_no_evalt::string_args

Definition at line 419 of file string_builtin_function.h.

◆ string_res

std::optional<array_string_exprt> string_builtin_function_with_no_evalt::string_res

Definition at line 418 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