43 const exprt &start_index,
44 const exprt &end_index)
58 fresh_symbol(
"QA_index_concat", res.
length().
type());
66 fresh_symbol(
"QA_index_concat2", res.
length().
type());
134 fresh_symbol, res,
s1,
s2, index_zero,
s2.length());
The type of an expression, extends irept.
Generates string constraints to link results from string functions with their arguments.
Application of (mathematical) function.
std::pair< exprt, string_constraintst > add_axioms_for_concat_substr(symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &start_index, const exprt &end_index)
Add axioms enforcing that res is the concatenation of s1 with the substring of s2 starting at index â...
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
array_string_exprt fresh_string(const typet &index_type, const typet &char_type)
construct a string expression whose length and content are new variables
Generation of fresh symbols of a given type.
The trinary if-then-else operator.
typet & type()
Return the type of the expression.
exprt length_constraint_for_concat_substr(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &start, const exprt &end)
Add axioms enforcing that the length of res is that of the concatenation of s1 with the substring of ...
signedbv_typet get_return_code_type()
Correspondance between arrays and pointers string representations.
Collection of constraints of different types: existential formulas, universal formulas, and "not contains" (universal with one alternation).
exprt minimum(const exprt &a, const exprt &b)
std::pair< exprt, string_constraintst > add_axioms_for_concat_code_point(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Add axioms corresponding to the StringBuilder.appendCodePoint(I) function.
std::pair< exprt, string_constraintst > combine_results(std::pair< exprt, string_constraintst > result1, std::pair< exprt, string_constraintst > result2)
Combine the results of two add_axioms function by taking the maximum of the return codes and merging ...
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 length_constraint_for_concat_char(const array_string_exprt &res, const array_string_exprt &s1)
Add axioms enforcing that the length of res is that of the concatenation of s1 with.
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 ...
#define PRECONDITION(CONDITION)
The plus expression Associativity is not specified.
std::pair< exprt, string_constraintst > add_axioms_for_concat(symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
Add axioms enforcing that res is equal to the concatenation of s1 and s2.
bitvector_typet index_type()
exprt maximum(const exprt &a, const exprt &b)
std::vector< exprt > existential
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
exprt length_constraint_for_concat(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
Add axioms enforcing that the length of res is that of the concatenation of s1 with s2 ...
const array_string_exprt & char_array_of_pointer(array_poolt &pool, const exprt &pointer, const exprt &length)
Adds creates a new array if it does not already exists.
Base class for all expressions.
std::vector< string_constraintt > universal
Universally quantified string constraint
exprt sum_overflows(const plus_exprt &sum)
Expression to hold a symbol (variable)
const typet & subtype() const
bitvector_typet char_type()