cprover
string_constraint_generator_code_points.cpp File Reference
+ Include dependency graph for string_constraint_generator_code_points.cpp:

Go to the source code of this file.

Functions

std::pair< exprt, string_constraintstadd_axioms_for_code_point (const array_string_exprt &res, const exprt &code_point)
 add axioms for the conversion of an integer representing a java code point to a utf-16 string More...
 
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...
 
std::pair< exprt, string_constraintstadd_axioms_for_code_point_at (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 add axioms corresponding to the String.codePointAt java function More...
 
std::pair< exprt, string_constraintstadd_axioms_for_code_point_before (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 add axioms corresponding to the String.codePointBefore java function More...
 
std::pair< exprt, string_constraintstadd_axioms_for_code_point_count (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 add axioms giving approximate bounds on the result of the String.codePointCount java function More...
 
std::pair< exprt, string_constraintstadd_axioms_for_offset_by_code_point (symbol_generatort &fresh_symbol, const function_application_exprt &f)
 add axioms giving approximate bounds on the result of the String.offsetByCodePointCount java function. More...
 

Detailed Description

Generates string constraints for Java functions dealing with code points

Definition in file string_constraint_generator_code_points.cpp.

Function Documentation

◆ add_axioms_for_code_point()

std::pair<exprt, string_constraintst> add_axioms_for_code_point ( const array_string_exprt res,
const exprt code_point 
)

add axioms for the conversion of an integer representing a java code point to a utf-16 string

Parameters
resarray of characters corresponding to the result fo the function
code_pointan expression representing a java code point
Returns
integer expression equal to zero

Definition at line 20 of file string_constraint_generator_code_points.cpp.

◆ add_axioms_for_code_point_at()

std::pair<exprt, string_constraintst> add_axioms_for_code_point_at ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

add axioms corresponding to the String.codePointAt java function

Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with arguments a string and an index
array_poolpool of arrays representing strings
Returns
a integer expression corresponding to a code point

Definition at line 122 of file string_constraint_generator_code_points.cpp.

◆ add_axioms_for_code_point_before()

std::pair<exprt, string_constraintst> add_axioms_for_code_point_before ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

add axioms corresponding to the String.codePointBefore java function

parameters: function application with two arguments: a string and an
index
Returns
a integer expression corresponding to a code point

Definition at line 155 of file string_constraint_generator_code_points.cpp.

◆ add_axioms_for_code_point_count()

std::pair<exprt, string_constraintst> add_axioms_for_code_point_count ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

add axioms giving approximate bounds on the result of the String.codePointCount java function

Add axioms corresponding the String.codePointCount java function.

Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with three arguments string str, integer begin and integer end.
array_poolpool of arrays representing strings
Returns
an integer expression

Definition at line 193 of file string_constraint_generator_code_points.cpp.

◆ add_axioms_for_offset_by_code_point()

std::pair<exprt, string_constraintst> add_axioms_for_offset_by_code_point ( symbol_generatort fresh_symbol,
const function_application_exprt f 
)

add axioms giving approximate bounds on the result of the String.offsetByCodePointCount java function.

Add axioms corresponding the String.offsetByCodePointCount java function.

We approximate the result by saying the result is between index + offset and index + 2 * offset

Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with arguments string str, integer index and integer offset.
Returns
a new string expression

Definition at line 222 of file string_constraint_generator_code_points.cpp.

◆ 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
chra character expression
Returns
a Boolean expression

Definition at line 76 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
chra character expression
Returns
a Boolean expression

Definition at line 89 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
char1a character expression
char2a character expression
return_typetype of the expression to return
Returns
an integer expression of type return_type

Definition at line 105 of file string_constraint_generator_code_points.cpp.