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.

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_transformation_builtin_functiont

string_transformation_builtin_functiont (exprt return_code, array_string_exprt result, array_string_exprt input, array_poolt &array_pool)

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.

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

std::vector< array_string_exprt > string_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.

- 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

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, array_poolt &array_pool)

- Protected Attributes inherited from string_builtin_functiont

array_poolt & array_pool

Detailed Description

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

Definition at line 285 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 289 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,

array_poolt & array_pool

)

inline

Definition at line 297 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,

message_handlert & message_handler

) 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:

res.length = str.length && return_code = 0
forall i < str.length. is_lower_case(str[i]) ? res[i] = str[i] - 0x20 : res[i] = str[i]

Parameters: fresh_symbol generator of fresh symbols

message_handler message handler

Returns: set of constraints

Definition at line 343 of file string_builtin_function.cpp.

◆ constraints() [2/2]

string_constraintst string_to_upper_case_builtin_functiont::constraints ( string_constraint_generatort & ,

message_handlert &

) const

inlineoverridevirtual

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

◆ eval()

std::optional< 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 316 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 329 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 313 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