22 const exprt &code_point)
134 const symbol_exprt result = fresh_symbol(
"char", return_type);
140 const exprt pair =
pair_value(char1_as_int, char2_as_int, return_type);
148 return {result, constraints};
175 const exprt pair =
pair_value(char1_as_int, char2_as_int, return_type);
183 return {result, constraints};
204 const symbol_exprt result = fresh_symbol(
"code_point_count", return_type);
207 constraints.existential.push_back(
209 constraints.existential.push_back(
212 return {result, constraints};
231 const symbol_exprt result = fresh_symbol(
"offset_by_code_point", return_type);
235 constraints.existential.push_back(
237 constraints.existential.push_back(
240 return {result, constraints};
The type of an expression, extends irept.
Semantic type conversion.
Generates string constraints to link results from string functions with their arguments.
A base class for relations, i.e., binary predicates.
Application of (mathematical) function.
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
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...
Generation of fresh symbols of a given type.
typet & type()
Return the type of the expression.
signedbv_typet get_return_code_type()
Correspondance between arrays and pointers string representations.
Collection of constraints of different types: existential formulas, universal formulas,...
exprt minimum(const exprt &a, const exprt &b)
const irep_idt & id() const
array_string_exprt get_string_expr(array_poolt &pool, const exprt &expr)
casts an expression to a string expression, or fetches the actual string_exprt in the case of a symbo...
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...
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....
exprt::operandst argumentst
#define PRECONDITION(CONDITION)
The plus expression Associativity is not specified.
Binary multiplication Associativity is not specified.
exprt maximum(const exprt &a, const exprt &b)
std::vector< exprt > existential
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....
equal_exprt length_eq(const T &lhs, const exprt &rhs)
Base class for all expressions.
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
Expression to hold a symbol (variable)
const typet & subtype() const
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
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
bitvector_typet char_type()