cprover
string_constraint_generator_code_points.cpp File Reference

Generates string constraints for Java functions dealing with code points. More...

Include dependency graph for string_constraint_generator_code_points.cpp:

Go to the source code of this file.

Functions

exprt pair_value (exprt char1, exprt char2, typet return_type)
 the output corresponds to the unicode character given by the pair of characters of inputs assuming it has been encoded in UTF-16, see https://en.wikipedia.org/wiki/UTF-16 for more explenation about the encoding; the operation we perform is: pair_value=0x10000+(((char1%0x0800)*0x0400)+char2%0x0400) More...
 

Detailed Description

Generates string constraints for Java functions dealing with code points.

Definition in file string_constraint_generator_code_points.cpp.

Function Documentation

◆ pair_value()

exprt pair_value ( exprt  char1,
exprt  char2,
typet  return_type 
)

the output corresponds to the unicode character given by the pair of characters of inputs assuming it has been encoded in UTF-16, see https://en.wikipedia.org/wiki/UTF-16 for more explenation about the encoding; the operation we perform is: pair_value=0x10000+(((char1%0x0800)*0x0400)+char2%0x0400)

Parameters
char1a character expression
char2a character expression
return_typetype of the expression to return
Returns
an integer expression of type return_type

Definition at line 104 of file string_constraint_generator_code_points.cpp.

References from_integer().

Referenced by string_constraint_generatort::add_axioms_for_code_point_at(), string_constraint_generatort::add_axioms_for_code_point_before(), and character_refine_preprocesst::convert_to_code_point().