134 DEPRECATED(
"should convert the value to string and call insert")
141 char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
142 const exprt &offset = f.arguments()[3];
146 exprt return_code = add_axioms_from_int(
s2, f.arguments()[4]);
147 return add_axioms_for_insert(res,
s1,
s2, offset);
155 DEPRECATED(
"should convert the value to string and call insert")
162 char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
163 const exprt &offset = f.arguments()[3];
167 exprt return_code = add_axioms_from_bool(
s2, f.arguments()[4]);
168 return add_axioms_for_insert(res,
s1,
s2, offset);
196 DEPRECATED(
"should convert the value to string and call insert")
202 char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
204 const exprt &offset = f.arguments()[3];
208 const exprt return_code =
209 add_axioms_for_string_of_float(
s2, f.arguments()[4]);
210 return add_axioms_for_insert(res,
s1,
s2, offset);
218 DEPRECATED(
"should convert the value to string and call insert")
222 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)
DEPRECATED("use instrument_cover_goals(goto_programt &goto_program," "const cover_instrumenterst &instrumenters," "message_handlert &message_handler, const irep_idt mode) instead") void instrument_cover_goals(const symbol_tablet &symbol_table
Instruments goto program for a given coverage criterion.
#define PRECONDITION(CONDITION)
bitvector_typet index_type()
exprt maximum(const exprt &a, const exprt &b)
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(st...
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, const exprt &offset)
Add axioms ensuring the length of res corresponds that of s1 where we inserted s2 at position offset...
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