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: two character expressions and a return type
char1 and char2 should be of type return_type
Returns
an integer expression of type return_type

Definition at line 110 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().