cprover
string_to_upper_case_builtin_functiont Class Reference

Converting each lowercase character of Basic Latin and Latin-1 supplement to the corresponding uppercase character. More...

#include <string_builtin_function.h>

+ Inheritance diagram for string_to_upper_case_builtin_functiont:
+ Collaboration diagram for string_to_upper_case_builtin_functiont:

Public Member Functions

 string_to_upper_case_builtin_functiont (const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
 
 string_to_upper_case_builtin_functiont (exprt return_code, array_string_exprt result, array_string_exprt input)
 
optionalt< exprteval (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. More...
 
std::string name () const override
 
string_constraintst constraints (class symbol_generatort &fresh_symbol) const
 Set of constraints ensuring result corresponds to input in which lowercase characters of Basic Latin and Latin-1 supplement of unicode have been converted to uppercase. 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_transformation_builtin_functiont
 string_transformation_builtin_functiont (exprt return_code, array_string_exprt result, array_string_exprt input)
 
 string_transformation_builtin_functiont (const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
 Constructor from arguments of a function application. More...
 
optionalt< array_string_exprtstring_result () const override
 
std::vector< array_string_exprtstring_arguments () 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. More...
 
- Public Member Functions inherited from string_builtin_functiont
 string_builtin_functiont (const string_builtin_functiont &)=delete
 
virtual ~string_builtin_functiont ()=default
 

Additional Inherited Members

- Public Attributes inherited from string_transformation_builtin_functiont
array_string_exprt result
 
array_string_exprt input
 
- Public Attributes inherited from string_builtin_functiont
exprt return_code
 
- Protected Member Functions inherited from string_builtin_functiont
 string_builtin_functiont (exprt return_code)
 

Detailed Description

Converting each lowercase character of Basic Latin and Latin-1 supplement to the corresponding uppercase character.

Definition at line 223 of file string_builtin_function.h.

Constructor & Destructor Documentation

◆ string_to_upper_case_builtin_functiont() [1/2]

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

Definition at line 227 of file string_builtin_function.h.

◆ string_to_upper_case_builtin_functiont() [2/2]

string_to_upper_case_builtin_functiont::string_to_upper_case_builtin_functiont ( exprt  return_code,
array_string_exprt  result,
array_string_exprt  input 
)
inline

Definition at line 235 of file string_builtin_function.h.

Member Function Documentation

◆ constraints() [1/2]

string_constraintst string_to_upper_case_builtin_functiont::constraints ( class symbol_generatort fresh_symbol) const

Set of constraints ensuring result corresponds to input in which lowercase characters of Basic Latin and Latin-1 supplement of unicode have been converted to uppercase.

These constraints are:

  1. res.length = str.length && return_code = 0
  2. forall i < str.length. is_lower_case(str[i]) ? res[i] = str[i] - 0x20 : res[i] = str[i]
Parameters
fresh_symbolgenerator of fresh symbols
Returns
set of constraints

Definition at line 422 of file string_builtin_function.cpp.

◆ constraints() [2/2]

string_constraintst string_to_upper_case_builtin_functiont::constraints ( string_constraint_generatort constraint_generator) const
inlineoverridevirtual

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 257 of file string_builtin_function.h.

◆ eval()

optionalt< exprt > string_to_upper_case_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 396 of file string_builtin_function.cpp.

◆ length_constraint()

exprt string_to_upper_case_builtin_functiont::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 262 of file string_builtin_function.h.

◆ name()

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

Implements string_builtin_functiont.

Definition at line 249 of file string_builtin_function.h.


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