135 DEPRECATED(
"should convert the value to string and call insert")
142 char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
143 const exprt &offset = f.arguments()[3];
147 exprt return_code = add_axioms_for_string_of_int(
s2, f.arguments()[4]);
148 return add_axioms_for_insert(res,
s1,
s2, offset);
156 DEPRECATED(
"should convert the value to string and call insert")
163 char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
164 const exprt &offset = f.arguments()[3];
168 exprt return_code = add_axioms_from_bool(
s2, f.arguments()[4]);
169 return add_axioms_for_insert(res,
s1,
s2, offset);
197 DEPRECATED(
"should convert the value to string and call insert")
203 char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
205 const exprt &offset = f.arguments()[3];
209 const exprt return_code =
210 add_axioms_for_string_of_float(
s2, f.arguments()[4]);
211 return add_axioms_for_insert(res,
s1,
s2, offset);
219 DEPRECATED(
"should convert the value to string and call insert")
223 return add_axioms_for_insert_double(f);
The type of an expression.
exprt add_axioms_for_insert(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &offset)
Add axioms ensuring the result res corresponds to s1 where we inserted s2 at position offset...
Generates string constraints to link results from string functions with their arguments.
application of (mathematical) function
const signedbv_typet get_return_code_type()
The trinary if-then-else operator.
exprt minimum(const exprt &a, const exprt &b)
#define PRECONDITION(CONDITION)
bitvector_typet index_type()
exprt maximum(const exprt &a, const exprt &b)
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
exprt add_axioms_for_substring(const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end)
Add axioms ensuring that res corresponds to the substring of str between indexes ‘start’ = max(star...
Base class for all expressions.
exprt length_constraint_for_insert(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
Add axioms ensuring the length of res corresponds to that of s1 where we inserted s2...
Universally quantified string constraint
std::vector< exprt > lemmas
Expression to hold a symbol (variable)
const array_string_exprt & char_array_of_pointer(const exprt &pointer, const exprt &length)
Adds creates a new array if it does not already exists.
const typet & subtype() const
std::vector< string_constraintt > constraints
array_string_exprt fresh_string(const typet &index_type, const typet &char_type)
construct a string expression whose length and content are new variables
exprt add_axioms_from_char(const function_application_exprt &f)
Conversion from char to string.
bitvector_typet char_type()
array_string_exprt get_string_expr(const exprt &expr)
casts an expression to a string expression, or fetches the actual string_exprt in the case of a symbo...
exprt add_axioms_for_insert_char(const function_application_exprt &f)
Add axioms corresponding to the StringBuilder.insert(C) java function.
symbol_generatort fresh_symbol