36 : array_pool(fresh_symbol), ns(ns), message_handler(message_handler)
64 const exprt &return_code,
88 const exprt &return_code,
133 const std::string &char_set)
142 const exprt chr = s[qvar];
149 return {{}, {sc}, {}};
162 std::pair<exprt, string_constraintst>
197 const exprt &return_code,
201 if(
id == ID_cprover_associate_array_to_pointer_func)
203 else if(
id == ID_cprover_associate_length_to_array_func)
213 std::pair<exprt, string_constraintst>
219 if(
id == ID_cprover_char_literal_func)
221 else if(
id == ID_cprover_string_length_func)
223 else if(
id == ID_cprover_string_equal_func)
225 else if(
id == ID_cprover_string_equals_ignore_case_func)
227 else if(
id == ID_cprover_string_is_empty_func)
229 else if(
id == ID_cprover_string_char_at_func)
231 else if(
id == ID_cprover_string_is_prefix_func)
233 else if(
id == ID_cprover_string_is_suffix_func)
235 else if(
id == ID_cprover_string_startswith_func)
237 else if(
id == ID_cprover_string_endswith_func)
239 else if(
id == ID_cprover_string_contains_func)
241 else if(
id == ID_cprover_string_index_of_func)
243 else if(
id == ID_cprover_string_last_index_of_func)
246 id == ID_cprover_string_is_valid_int_func ||
247 id == ID_cprover_string_is_valid_long_func)
249 else if(
id == ID_cprover_string_parse_int_func)
251 else if(
id == ID_cprover_string_code_point_at_func)
253 else if(
id == ID_cprover_string_code_point_before_func)
255 else if(
id == ID_cprover_string_code_point_count_func)
257 else if(
id == ID_cprover_string_offset_by_code_point_func)
259 else if(
id == ID_cprover_string_compare_to_func)
261 else if(
id == ID_cprover_string_literal_func)
263 else if(
id == ID_cprover_string_concat_code_point_func)
265 else if(
id == ID_cprover_string_substring_func)
267 else if(
id == ID_cprover_string_trim_func)
269 else if(
id == ID_cprover_string_empty_string_func)
271 else if(
id == ID_cprover_string_copy_func)
273 else if(
id == ID_cprover_string_of_int_hex_func)
275 else if(
id == ID_cprover_string_of_float_func)
277 else if(
id == ID_cprover_string_of_float_scientific_notation_func)
279 else if(
id == ID_cprover_string_of_double_func)
281 else if(
id == ID_cprover_string_of_long_func)
283 else if(
id == ID_cprover_string_set_length_func)
285 else if(
id == ID_cprover_string_delete_func)
287 else if(
id == ID_cprover_string_delete_char_at_func)
289 else if(
id == ID_cprover_string_replace_func)
291 else if(
id == ID_cprover_string_constrain_characters_func)
296 "string_constraint_generator::function_application: unknown symbol :");
314 const auto &args = f.arguments();
321 args.size() == 3 ? array_pool.get_or_create_length(str) : args[4];
322 return add_axioms_for_substring(res, str, offset,
plus_exprt(offset, count));
330 std::pair<exprt, string_constraintst>
349 std::pair<exprt, string_constraintst>
357 const exprt &arg = args[0];
386 std::pair<exprt, string_constraintst>
396 return {std::move(char_sym), std::move(constraints)};
419 std::pair<exprt, string_constraintst>
421 std::pair<exprt, string_constraintst> result1,
422 std::pair<exprt, string_constraintst> result2)
424 const exprt return_code =
maximum(result1.first, result2.first);
425 merge(result2.second, std::move(result1.second));
array_string_exprt get_string_expr(array_poolt &array_pool, const exprt &expr)
Fetch the string_exprt corresponding to the given refined_string_exprt.
exprt get_or_create_length(const array_string_exprt &s)
Get the length of an array_string_exprt from the array_pool.
void insert(const exprt &pointer_expr, const array_string_exprt &array)
array_string_exprt find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
const typet & length_type() const
const typet & element_type() const
The type of the elements of the array.
A base class for relations, i.e., binary predicates whose two operands have the same type.
const irep_idt & get_value() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const char * c_str() const
Base class for all expressions.
typet & type()
Return the type of the expression.
Application of (mathematical) function.
exprt::operandst argumentst
The trinary if-then-else operator.
const irept & find(const irep_idt &name) const
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The plus expression Associativity is not specified.
Fixed-width bit-vector with two's complement interpretation.
void value(const irep_idt &)
std::pair< exprt, string_constraintst > add_axioms_for_empty_string(const function_application_exprt &f)
Add axioms to say that the returned string expression is empty.
std::pair< exprt, string_constraintst > add_axioms_for_compare_to(const function_application_exprt &f)
Lexicographic comparison of two strings.
std::pair< exprt, string_constraintst > add_axioms_for_equals_ignore_case(const function_application_exprt &f)
Equality of the content ignoring case of characters.
std::pair< exprt, string_constraintst > add_axioms_for_delete(const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end)
Add axioms stating that res corresponds to the input str where we removed characters between the posi...
std::pair< exprt, string_constraintst > add_axioms_for_last_index_of(const array_string_exprt &str, const exprt &c, const exprt &from_index)
Add axioms stating that the returned value is the index within haystack (str) of the last occurrence ...
std::pair< exprt, string_constraintst > add_axioms_from_double(const function_application_exprt &f)
Add axioms corresponding to the String.valueOf(D) java function.
exprt associate_array_to_pointer(const exprt &return_code, const function_application_exprt &f)
Associate a char array to a char pointer.
std::pair< exprt, string_constraintst > 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(start,...
std::pair< exprt, string_constraintst > add_axioms_for_equals(const function_application_exprt &f)
Equality of the content of two strings.
std::pair< exprt, string_constraintst > add_axioms_for_is_valid_int(const function_application_exprt &f)
Check a string is a valid integer, using the same rules as Java Integer.parseInt.
std::pair< exprt, string_constraintst > add_axioms_from_int_hex(const array_string_exprt &res, const exprt &i)
Add axioms stating that the string res corresponds to the integer argument written in hexadecimal.
std::pair< exprt, string_constraintst > add_axioms_for_is_empty(const function_application_exprt &f)
Add axioms stating that the returned value is true exactly when the argument string is empty.
std::optional< exprt > make_array_pointer_association(const exprt &return_code, const function_application_exprt &expr)
Associate array to pointer, and array to length.
std::pair< exprt, string_constraintst > add_axioms_for_index_of(const array_string_exprt &str, const exprt &c, const exprt &from_index)
Add axioms stating that the returned value is the index within haystack (str) of the first occurrence...
std::pair< exprt, string_constraintst > add_axioms_for_constrain_characters(const function_application_exprt &f)
Add axioms to ensure all characters of a string belong to a given set.
std::pair< exprt, string_constraintst > add_axioms_for_function_application(const function_application_exprt &expr)
strings contained in this call are converted to objects of type string_exprt, through adding axioms.
message_handlert & message_handler
std::pair< exprt, string_constraintst > add_axioms_for_set_length(const function_application_exprt &f)
Reduce or extend a string to have the given length.
std::pair< exprt, string_constraintst > add_axioms_for_offset_by_code_point(const function_application_exprt &f)
Add axioms corresponding the String.offsetByCodePointCount java function.
std::pair< exprt, string_constraintst > add_axioms_for_is_prefix(const array_string_exprt &prefix, const array_string_exprt &str, const exprt &offset)
Add axioms stating that the returned expression is true exactly when the offset is greater or equal t...
std::pair< exprt, string_constraintst > add_axioms_for_trim(const function_application_exprt &f)
Remove leading and trailing whitespaces.
std::pair< exprt, string_constraintst > add_axioms_for_replace(const function_application_exprt &f)
Replace a character by another in a string.
std::pair< exprt, string_constraintst > add_axioms_for_parse_int(const function_application_exprt &f)
Integer value represented by a string.
exprt associate_length_to_array(const exprt &return_code, const function_application_exprt &f)
Associate an integer length to a char array.
std::pair< exprt, string_constraintst > add_axioms_from_literal(const function_application_exprt &f)
String corresponding to an internal cprover string.
std::pair< exprt, string_constraintst > add_axioms_for_is_suffix(const function_application_exprt &f, bool swap_arguments)
Test if the target is a suffix of the string.
std::pair< exprt, string_constraintst > add_axioms_for_contains(const function_application_exprt &f)
Test whether a string contains another.
string_constraint_generatort(const namespacet &ns, message_handlert &message_handler)
symbol_generatort fresh_symbol
string_constraintst add_constraint_on_characters(const array_string_exprt &s, const exprt &start, const exprt &end, const std::string &char_set)
Add constraint on characters of a string.
std::pair< exprt, string_constraintst > add_axioms_from_float_scientific_notation(const array_string_exprt &res, const exprt &f)
Add axioms to write the float in scientific notation.
std::pair< exprt, string_constraintst > add_axioms_for_copy(const function_application_exprt &f)
add axioms to say that the returned string expression is equal to the argument of the function applic...
std::pair< exprt, string_constraintst > add_axioms_for_string_of_float(const function_application_exprt &f)
String representation of a float value.
std::pair< exprt, string_constraintst > add_axioms_from_long(const function_application_exprt &f)
Add axioms corresponding to the String.valueOf(J) java function.
std::pair< exprt, string_constraintst > add_axioms_for_code_point_count(const function_application_exprt &f)
Add axioms corresponding the String.codePointCount java function.
std::pair< exprt, string_constraintst > add_axioms_for_concat_code_point(const function_application_exprt &f)
Add axioms corresponding to the StringBuilder.appendCodePoint(I) function.
std::pair< exprt, string_constraintst > add_axioms_for_code_point_at(const function_application_exprt &f)
add axioms corresponding to the String.codePointAt java function
std::pair< exprt, string_constraintst > add_axioms_for_char_at(const function_application_exprt &f)
Character at a given position.
std::pair< exprt, string_constraintst > add_axioms_for_code_point_before(const function_application_exprt &f)
add axioms corresponding to the String.codePointBefore java function
std::pair< exprt, string_constraintst > add_axioms_for_delete_char_at(const function_application_exprt &expr)
add axioms corresponding to the StringBuilder.deleteCharAt java function
std::pair< exprt, string_constraintst > add_axioms_for_length(const function_application_exprt &f)
Length of a string.
std::pair< exprt, string_constraintst > add_axioms_for_char_literal(const function_application_exprt &f)
add axioms stating that the returned value is equal to the argument
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 ...
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
The type of an expression, extends irept.
#define SINCE(year, month, day, msg)
exprt interval_constraint(const exprt &expr, const integer_intervalt &interval)
Given an exprt and an integer interval return an exprt that represents restricting the expression to ...
const std::string & id2string(const irep_idt &d)
API to expression classes for 'mathematical' expressions.
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
bool is_ssa_expr(const exprt &expr)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const string_constantt & to_string_constant(const exprt &expr)
Generates string constraints to link results from string functions with their arguments.
exprt is_positive(const exprt &x)
static irep_idt get_function_name(const function_application_exprt &expr)
exprt sum_overflows(const plus_exprt &sum)
exprt maximum(const exprt &a, const exprt &b)
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
exprt minimum(const exprt &a, const exprt &b)
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
signedbv_typet get_return_code_type()
array_string_exprt & to_array_string_expr(exprt &expr)
#define string_refinement_invariantt(reason)
Collection of constraints of different types: existential formulas, universal formulas,...
std::vector< string_not_contains_constraintt > not_contains
std::vector< exprt > existential
std::vector< string_constraintt > universal