cprover
|
Generates string constraints for Java functions dealing with code points. More...
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... | |
Generates string constraints for Java functions dealing with code points.
Definition in file string_constraint_generator_code_points.cpp.
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)
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().