Go to the documentation of this file.
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};
#define PRECONDITION(CONDITION)
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
equal_exprt length_eq(const T &lhs, const exprt &rhs)
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
exprt minimum(const exprt &a, const exprt &b)
The type of an expression, extends irept.
Correspondance between arrays and pointers string representations.
The plus expression Associativity is not specified.
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....
Base class for all expressions.
Collection of constraints of different types: existential formulas, universal formulas,...
Expression to hold a symbol (variable)
exprt::operandst argumentst
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...
typet & type()
Return the type of the expression.
Generation of fresh symbols of a given type.
exprt maximum(const exprt &a, const exprt &b)
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....
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
Application of (mathematical) function.
Binary multiplication Associativity is not specified.
const irep_idt & id() const
signedbv_typet get_return_code_type()
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...
bitvector_typet char_type()
A base class for relations, i.e., binary predicates.
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
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...
Semantic type conversion.
std::vector< exprt > existential