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 More...
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 More...
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

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.