CBMC
Loading...
Searching...
No Matches
Public Member Functions | Private Attributes | List of all members
string_of_int_builtin_functiont Class Reference

String creation from integer types. More...

#include <string_builtin_function.h>

+ Inheritance diagram for string_of_int_builtin_functiont:
[フレーム]
[legend]
+ Collaboration diagram for string_of_int_builtin_functiont:
[フレーム]
[legend]

Public Member Functions

  string_of_int_builtin_functiont (const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
 
std::optional< exprt >  eval (const std::function< exprt(const exprt &)> &get_value) const override
  Given a function get_value which gives a valuation to expressions, attempt to find the result of the builtin function.
 
std::string  name () const override
 
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_creation_builtin_functiont
  string_creation_builtin_functiont (const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
  Constructor from arguments of a function application.
 
std::optional< array_string_exprt >  string_result () const override
 
bool  maybe_testing_function () const override
  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::vector< array_string_exprt >  string_arguments () const
 

Private Attributes

exprt  radix
 

Additional Inherited Members

- Public Attributes inherited from string_creation_builtin_functiont
array_string_exprt  result
 
exprt  arg
 
- Public Attributes inherited from string_builtin_functiont
exprt  return_code
 
- 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 creation from integer types.

Definition at line 363 of file string_builtin_function.h.

Constructor & Destructor Documentation

◆  string_of_int_builtin_functiont()

string_of_int_builtin_functiont::string_of_int_builtin_functiont ( const exprt &  return_code,
const std::vector< exprt > &  fun_args,
array_poolt &  array_pool 
)
inline

Definition at line 366 of file string_builtin_function.h.

Member Function Documentation

◆  constraints()

string_constraintst string_of_int_builtin_functiont::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 417 of file string_builtin_function.cpp.

◆  eval()

std::optional< exprt > string_of_int_builtin_functiont::eval ( const std::function< exprt(const exprt &)> &  get_value ) const
overridevirtual

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

◆  length_constraint()

exprt string_of_int_builtin_functiont::length_constraint ( ) const
overridevirtual

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

Implements string_builtin_functiont.

Definition at line 427 of file string_builtin_function.cpp.

◆  name()

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

Implements string_builtin_functiont.

Definition at line 382 of file string_builtin_function.h.

Member Data Documentation

◆  radix

exprt string_of_int_builtin_functiont::radix
private

Definition at line 394 of file string_builtin_function.h.

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

AltStyle によって変換されたページ (->オリジナル) /