Go to the documentation of this file.
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());
exprt sum_overflows(const plus_exprt &sum)
#define PRECONDITION(CONDITION)
const typet & subtype() const
exprt minimum(const exprt &a, const exprt &b)
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 ...
The type of an expression, extends irept.
Correspondance between arrays and pointers string representations.
The trinary if-then-else operator.
The plus expression Associativity is not specified.
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
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
Base class for all expressions.
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 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.
Collection of constraints of different types: existential formulas, universal formulas,...
Expression to hold a symbol (variable)
bitvector_typet index_type()
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 ...
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.
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)
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.
Application of (mathematical) function.
const irep_idt & id() const
signedbv_typet get_return_code_type()
bitvector_typet char_type()
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
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.
array_string_exprt fresh_string(const typet &index_type, const typet &char_type)
construct a string expression whose length and content are new variables
std::vector< exprt > existential
std::vector< string_constraintt > universal