21 assert(offset.
type()==
s1.length().type());
152 length,
data, offset, count);
string_exprt add_axioms_for_insert_char(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(C) java function
string_exprt add_axioms_for_insert_int(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(I) java function
Generates string constraints to link results from string functions with their arguments.
application of (mathematical) function
string_exprt add_axioms_from_bool(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(Z) java function
string_exprt add_axioms_for_insert_float(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(F) java function
string_exprt add_axioms_for_insert_long(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(J) java function
const std::size_t MAX_INTEGER_LENGTH
const std::size_t MAX_LONG_LENGTH
string_exprt add_axioms_for_insert_double(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(D) java function
string_exprt add_axioms_from_float(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(F) java function
string_exprt add_axioms_for_string_expr(const exprt &expr)
obtain a refined string expression corresponding to string variable of string function call ...
const refined_string_typet & to_refined_string_type(const typet &type)
string_exprt add_axioms_for_insert_bool(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(Z) java function
string_exprt add_axioms_for_concat(const string_exprt &s1, const string_exprt &s2)
add axioms to say that the returned string expression is equal to the concatenation of the two string...
string_exprt add_axioms_for_insert(const string_exprt &s1, const string_exprt &s2, const exprt &offset)
add axioms stating that the result correspond to the first string where we inserted the second one at...
string_exprt add_axioms_from_char(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(C) java function
Base class for all expressions.
string_exprt add_axioms_from_int(const function_application_exprt &f)
add axioms corresponding to the String.valueOf(I) java function
static const function_application_exprt::argumentst & args(const function_application_exprt &expr, size_t nb)
string_exprt add_axioms_for_insert_char_array(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert:(I[CII) and StringBuilder.insert:(I[C) java func...
string_exprt add_axioms_from_char_array(const function_application_exprt &f)
add axioms corresponding to the String.
string_exprt add_axioms_for_substring(const string_exprt &str, const exprt &start, const exprt &end)
add axioms stating that the returned string expression is equal to the input one starting at start an...