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

String creation from other types. More...

#include <string_builtin_function.h>

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

Public Member Functions

  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
 
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.
 
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.
 
virtual exprt  length_constraint () const =0
  Constraint ensuring that the length of the strings are coherent with the function call.
 

Public Attributes

array_string_exprt  result
 
exprt  arg
 
- 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 creation from other types.

Definition at line 340 of file string_builtin_function.h.

Constructor & Destructor Documentation

◆  string_creation_builtin_functiont()

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.

The arguments in fun_args should be in order: an integer result.length, a character pointer &result[0], an expression arg which is to be converted to a string. Other arguments are ignored by this constructor.

Definition at line 372 of file string_builtin_function.cpp.

Member Function Documentation

◆  maybe_testing_function()

bool string_creation_builtin_functiont::maybe_testing_function ( ) const
inlineoverridevirtual

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.

Reimplemented from string_builtin_functiont.

Definition at line 356 of file string_builtin_function.h.

◆  string_result()

std::optional< array_string_exprt > string_creation_builtin_functiont::string_result ( ) const
inlineoverridevirtual

Reimplemented from string_builtin_functiont.

Definition at line 351 of file string_builtin_function.h.

Member Data Documentation

◆  arg

exprt string_creation_builtin_functiont::arg

Definition at line 344 of file string_builtin_function.h.

◆  result

array_string_exprt string_creation_builtin_functiont::result

Definition at line 343 of file string_builtin_function.h.

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

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