Loading...

Searching...

No Matches

string_constraint_generator_code_points.cpp File Reference

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

#include "string_constraint_generator.h"
#include <util/mathematical_expr.h>

+ Include dependency graph for string_constraint_generator_code_points.cpp:

[フレーム]

Go to the source code of this file.

Functions

static exprt is_high_surrogate (const exprt &chr)

the output is true when the character is a high surrogate for UTF-16 encoding, see https://en.wikipedia.org/wiki/UTF-16 for more explenation about the encoding; this is true when the character is in the range 0xD800..0xDBFF

static exprt is_low_surrogate (const exprt &chr)

the output is true when the character is a low surrogate for UTF-16 encoding, see https://en.wikipedia.org/wiki/UTF-16 for more explenation about the encoding; this is true when the character is in the range 0xDC00..0xDFFF

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)

Detailed Description

Generates string constraints for Java functions dealing with code points.

Definition in file string_constraint_generator_code_points.cpp.

Function Documentation

◆ is_high_surrogate()

static exprt is_high_surrogate ( const exprt & chr )

static

the output is true when the character is a high surrogate for UTF-16 encoding, see https://en.wikipedia.org/wiki/UTF-16 for more explenation about the encoding; this is true when the character is in the range 0xD800..0xDBFF

Parameters: chr a character expression

Returns: a Boolean expression

Definition at line 80 of file string_constraint_generator_code_points.cpp.

◆ is_low_surrogate()

static exprt is_low_surrogate ( const exprt & chr )

static

the output is true when the character is a low surrogate for UTF-16 encoding, see https://en.wikipedia.org/wiki/UTF-16 for more explenation about the encoding; this is true when the character is in the range 0xDC00..0xDFFF

Parameters: chr a character expression

Returns: a Boolean expression

Definition at line 93 of file string_constraint_generator_code_points.cpp.

◆ 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: char1 a character expression

char2 a character expression

return_type type of the expression to return

Returns: an integer expression of type return_type

Definition at line 109 of file string_constraint_generator_code_points.cpp.