cprover
string_constraint_generator.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Generates string constraints to link results from string functions
4  with their arguments. This is inspired by the PASS paper at HVC'13:
5  "PASS: String Solving with Parameterized Array and Interval Automaton"
6  by Guodong Li and Indradeep Ghosh, which gives examples of constraints
7  for several functions.
8 
9 Author: Romain Brenguier, romain.brenguier@diffblue.com
10 
11 \*******************************************************************/
12 
19 
20 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_GENERATOR_H
21 #define CPROVER_SOLVERS_REFINEMENT_STRING_CONSTRAINT_GENERATOR_H
22 
23 #include <limits>
24 #include <util/string_expr.h>
25 #include <util/replace_expr.h>
27 #include <util/constexpr.def>
28 #include <util/deprecate.h>
30 
32 class symbol_generatort final
33 {
34 public:
36  operator()(const irep_idt &prefix, const typet &type = bool_typet());
37 
38 private:
39  unsigned symbol_count = 0;
40 };
41 
43 class array_poolt final
44 {
45 public:
46  explicit array_poolt(symbol_generatort &symbol_generator)
47  : fresh_symbol(symbol_generator)
48  {
49  }
50 
51  const std::unordered_map<exprt, array_string_exprt, irep_hash> &
53  {
54  return arrays_of_pointers;
55  }
56 
57  exprt get_length(const array_string_exprt &s) const;
58 
59  void insert(const exprt &pointer_expr, array_string_exprt &array);
60 
61  array_string_exprt find(const exprt &pointer, const exprt &length);
62 
64 
70 
71 private:
72  // associate arrays to char pointers
73  std::unordered_map<exprt, array_string_exprt, irep_hash> arrays_of_pointers;
74 
75  // associate length to arrays of infinite size
76  std::unordered_map<array_string_exprt, symbol_exprt, irep_hash>
78 
79  // generates fresh symbols
81 
83  const exprt &char_pointer,
84  const typet &char_array_type);
85 };
86 
88 {
89 public:
90  // This module keeps a list of axioms. It has methods which generate
91  // string constraints for different string functions and add them
92  // to the axiom list.
93 
94  // Used by format function
95  class format_specifiert;
96 
98 
101  const std::vector<exprt> &get_lemmas() const;
102  void add_lemma(const exprt &);
103  const std::vector<string_constraintt> &get_constraints() const;
104  const std::vector<string_not_contains_constraintt> &
106 
108  void clear_constraints();
109 
111  const std::vector<symbol_exprt> &get_boolean_symbols() const;
112 
114  const std::vector<symbol_exprt> &get_index_symbols() const;
115 
117  const std::set<array_string_exprt> &get_created_strings() const;
118 
121  const exprt &univ_val) const
122  {
123  return index_exprt(witness.at(c), univ_val);
124  }
125 
127  const function_application_exprt &expr);
128 
130 
131  symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type);
132 
133  symbol_exprt fresh_exist_index(const irep_idt &prefix, const typet &type);
134 
136 
142 
143  // Type used by primitives to signal errors
145  {
146  return signedbv_typet(32);
147  }
148 
150  const array_string_exprt &res,
151  const array_string_exprt &s1,
152  const exprt &c);
154  const array_string_exprt &res,
155  const array_string_exprt &s1,
156  const array_string_exprt &s2);
158  const array_string_exprt &res,
159  const array_string_exprt &s1,
160  const array_string_exprt &s2,
161  const exprt &start_index,
162  const exprt &end_index);
164  const array_string_exprt &res,
165  const array_string_exprt &s1,
166  const array_string_exprt &s2,
167  const exprt &offset);
169  const array_string_exprt &res,
170  const exprt &input_int,
171  const exprt &radix,
172  size_t max_size = 0);
174  const array_string_exprt &res,
175  const array_string_exprt &str,
176  const exprt &position,
177  const exprt &character);
179  const array_string_exprt &res,
180  const array_string_exprt &str);
182  const array_string_exprt &res,
183  const array_string_exprt &expr);
184 
185 private:
186  symbol_exprt fresh_boolean(const irep_idt &prefix);
188  fresh_string(const typet &index_type, const typet &char_type);
190 
191  static constant_exprt constant_char(int i, const typet &char_type);
192 
193  const array_string_exprt &
194  char_array_of_pointer(const exprt &pointer, const exprt &length);
195 
197 
199  const array_string_exprt &s,
200  const exprt &start,
201  const exprt &end,
202  const std::string &char_set);
203  exprt
205 
206  // The following functions add axioms for the returned value
207  // to be equal to the result of the function given as argument.
208  // They are not accessed directly from other classes: they call
209  // `add_axioms_for_function_application` which determines which of
210  // these methods should be called.
211 
218 
219  // Add axioms corresponding to the String.hashCode java function
220  // The specification is partial: the actual value is not actually computed
221  // but we ensure that hash codes of equal strings are equal.
223 
226  const array_string_exprt &prefix,
227  const array_string_exprt &str,
228  const exprt &offset);
230  const function_application_exprt &f, bool swap_arguments=false);
232  const function_application_exprt &f, bool swap_arguments=false);
241  const array_string_exprt &res,
242  irep_idt sval,
243  const exprt &guard = true_exprt());
244 
246  const array_string_exprt &res,
247  const array_string_exprt &str,
248  const exprt &start,
249  const exprt &end);
254  const array_string_exprt &res,
255  const std::string &s,
256  const exprt::operandst &args);
257 
259  const format_specifiert &fs,
260  const struct_exprt &arg,
261  const typet &index_type,
262  const typet &char_type);
263 
270 
272  const array_string_exprt &res,
273  const exprt &arg,
274  const exprt &guard);
278  const array_string_exprt &res,
279  const exprt &input_int,
280  size_t max_size = 0);
285  exprt add_axioms_from_bool(const array_string_exprt &res, const exprt &i);
287  exprt add_axioms_from_char(const array_string_exprt &res, const exprt &i);
289  const array_string_exprt &str,
290  const exprt &c,
291  const exprt &from_index);
293  const array_string_exprt &haystack,
294  const array_string_exprt &needle,
295  const exprt &from_index);
298  const array_string_exprt &haystack,
299  const array_string_exprt &needle,
300  const exprt &from_index);
302  const array_string_exprt &str,
303  const exprt &c,
304  const exprt &from_index);
305 
307 
314  exprt
317  const array_string_exprt &res,
318  const exprt &i,
319  size_t max_size);
321  const array_string_exprt &res,
322  const exprt &f);
324  const function_application_exprt &f);
325 
329 
332 
337  const array_string_exprt &res,
338  const array_string_exprt &str,
339  const exprt &start,
340  const exprt &end);
345 
347  const array_string_exprt &res,
348  const exprt &code_point);
350 
355  DEPRECATED("This is Java specific and should be implemented in Java")
357 
365  const function_application_exprt &f);
366 
368  const exprt &input_int,
369  const typet &type,
370  const bool strict_formatting,
371  const array_string_exprt &str,
372  const std::size_t max_string_length,
373  const exprt &radix,
374  const unsigned long radix_ul);
376  const array_string_exprt &str,
377  const exprt &radix_as_char,
378  const unsigned long radix_ul,
379  const std::size_t max_size,
380  const bool strict_formatting);
383 
389 
391 
393 
394  // Helper functions
395  static exprt int_of_hex_char(const exprt &chr);
396  static exprt is_high_surrogate(const exprt &chr);
397  static exprt is_low_surrogate(const exprt &chr);
399  exprt char1, exprt char2, exprt char_a, exprt char_A, exprt char_Z);
400  unsigned long to_integer_or_default(const exprt &expr, unsigned long def);
401 
402  // MEMBERS
403 public:
404  // Used to store information about witnesses for not_contains constraints
406 private:
409 
410  std::vector<exprt> lemmas;
415  const namespacet ns;
416  // To each string on which hash_code was called we associate a symbol
417  // representing the return value of the hash_code function.
419 
420  // Pool used for the intern method
422 };
423 
425  const exprt &chr,
426  const bool strict_formatting,
427  const exprt &radix_as_char,
428  const unsigned long radix_ul);
429 
431  const exprt &chr,
432  const typet &char_type,
433  const typet &type,
434  const bool strict_formatting,
435  unsigned long radix_ul);
436 
437 size_t max_printed_string_length(const typet &type, unsigned long ul_radix);
438 
439 std::string
440 utf16_constant_array_to_java(const array_exprt &arr, std::size_t length);
441 
443 exprt minimum(const exprt &a, const exprt &b);
444 
446 exprt maximum(const exprt &a, const exprt &b);
447 
449 exprt sum_overflows(const plus_exprt &sum);
450 
452  const array_string_exprt &res,
453  const array_string_exprt &s1);
455  const array_string_exprt &res,
456  const array_string_exprt &s1,
457  const array_string_exprt &s2);
459  const array_string_exprt &res,
460  const array_string_exprt &s1,
461  const array_string_exprt &s2,
462  const exprt &start_index,
463  const exprt &end_index);
465  const array_string_exprt &res,
466  const array_string_exprt &s1,
467  const array_string_exprt &s2);
468 
469 exprt zero_if_negative(const exprt &expr);
470 #endif
exprt add_axioms_for_compare_to(const function_application_exprt &f)
Lexicographic comparison of two strings.
The type of an expression.
Definition: type.h:22
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...
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...
void add_axioms_for_correct_number_format(const array_string_exprt &str, const exprt &radix_as_char, const unsigned long radix_ul, const std::size_t max_size, const bool strict_formatting)
Add axioms making the return value true if the given string is a correct number in the given radix...
std::vector< string_not_contains_constraintt > not_contains_constraints
const std::set< array_string_exprt > & get_created_strings() const
Set of strings that have been created by the generator.
exprt add_axioms_for_code_point_at(const function_application_exprt &f)
add axioms corresponding to the String.codePointAt java function
void add_axioms_for_characters_in_integer_string(const exprt &input_int, const typet &type, const bool strict_formatting, const array_string_exprt &str, const std::size_t max_string_length, const exprt &radix, const unsigned long radix_ul)
Add axioms connecting the characters in the input string to the value of the output integer...
std::map< array_string_exprt, symbol_exprt > intern_of_string
application of (mathematical) function
Definition: std_expr.h:4529
const std::vector< string_constraintt > & get_constraints() const
exprt get_witness_of(const string_not_contains_constraintt &c, const exprt &univ_val) const
exprt add_axioms_from_literal(const function_application_exprt &f)
String corresponding to an internal cprover string.
exprt add_axioms_from_int(const function_application_exprt &f)
Convert an integer to a string.
exprt add_axioms_for_empty_string(const function_application_exprt &f)
Add axioms to say that the returned string expression is empty.
exprt add_axioms_for_equals(const function_application_exprt &f)
Equality of the content of two strings.
exprt add_axioms_for_length(const function_application_exprt &f)
Length of a string.
exprt add_axioms_for_insert_float(const function_application_exprt &f)
Add axioms corresponding to the StringBuilder.insert(F) java function.
Type for string expressions used by the string solver.
const std::vector< exprt > & get_lemmas() const
Axioms are of three kinds: universally quantified string constraint, not contains string constraints ...
std::map< array_string_exprt, exprt > hash_code_of_string
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.
Generation of fresh symbols of a given type.
array_poolt(symbol_generatort &symbol_generator)
std::unordered_map< exprt, array_string_exprt, irep_hash > arrays_of_pointers
exprt add_axioms_for_contains(const function_application_exprt &f)
Test whether a string contains another.
exprt add_axioms_for_code_point_count(const function_application_exprt &f)
Add axioms corresponding the String.codePointCount java function.
exprt add_axioms_for_offset_by_code_point(const function_application_exprt &f)
Add axioms corresponding the String.offsetByCodePointCount java function.
symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type)
generate an index symbol to be used as an universaly quantified variable
exprt associate_array_to_pointer(const function_application_exprt &f)
Associate a char array to a char pointer.
exprt get_length(const array_string_exprt &s) const
Associate an actual finite length to infinite arrays.
std::vector< symbol_exprt > boolean_symbols
exprt is_digit_with_radix(const exprt &chr, const bool strict_formatting, const exprt &radix_as_char, const unsigned long radix_ul)
Check if a character is a digit with respect to the given radix, e.g.
exprt associate_length_to_array(const function_application_exprt &f)
Associate an integer length to a char array.
exprt add_axioms_for_to_upper_case(const array_string_exprt &res, const array_string_exprt &expr)
Add axioms ensuring res corresponds to str in which lowercase characters of Basic Latin and Latin-1 s...
STL namespace.
exprt add_axioms_from_long(const function_application_exprt &f)
Add axioms corresponding to the String.valueOf(J) java function.
const std::vector< string_not_contains_constraintt > & get_not_contains_constraints() const
The proper Booleans.
Definition: std_types.h:34
A constant literal expression.
Definition: std_expr.h:4422
Correspondance between arrays and pointers string representations.
exprt 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...
exprt add_axioms_for_trim(const function_application_exprt &f)
Remove leading and trailing whitespaces.
exprt 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...
exprt minimum(const exprt &a, const exprt &b)
void clear_constraints()
Clear all constraints and lemmas.
const std::vector< symbol_exprt > & get_boolean_symbols() const
Boolean symbols for the results of some string functions.
exprt 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...
exprt add_axioms_from_int_hex(const array_string_exprt &res, const exprt &i)
exprt add_axioms_from_double(const function_application_exprt &f)
Add axioms corresponding to the String.valueOf(D) java function.
exprt add_axioms_for_string_of_int_with_radix(const array_string_exprt &res, const exprt &input_int, const exprt &radix, size_t max_size=0)
Add axioms enforcing that the string corresponds to the result of String.valueOf(II) or String...
symbol_exprt fresh_boolean(const irep_idt &prefix)
generate a Boolean symbol which is existentially quantified
exprt add_axioms_from_float_scientific_notation(const array_string_exprt &res, const exprt &f)
Add axioms to write the float in scientific notation.
exprt add_axioms_for_to_lower_case(const array_string_exprt &res, const array_string_exprt &str)
Add axioms ensuring res corresponds to str in which uppercase characters have been converted to lower...
array_string_exprt find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
The boolean constant true.
Definition: std_expr.h:4486
exprt add_axioms_for_constant(const array_string_exprt &res, irep_idt sval, const exprt &guard=true_exprt())
Add axioms ensuring that the provided string expression and constant are equal.
Constraints to encode non containement of strings.
Defines string constraints.
exprt add_axioms_for_hash_code(const function_application_exprt &f)
Value that is identical for strings with the same content.
exprt add_axioms_for_delete_char_at(const function_application_exprt &expr)
add axioms corresponding to the StringBuilder.deleteCharAt java function
exprt add_axioms_for_index_of_string(const array_string_exprt &haystack, const array_string_exprt &needle, const exprt &from_index)
Add axioms stating that the returned value index is the index within haystack of the first occurrence...
std::vector< symbol_exprt > index_symbols
symbol_exprt add_axioms_for_intern(const function_application_exprt &f)
Add axioms corresponding to the String.intern java function.
Fixed-width bit-vector with two&#39;s complement interpretation.
Definition: std_types.h:1271
exprt add_axioms_for_replace(const function_application_exprt &f)
Replace a character by another in a string.
exprt add_axioms_for_parse_int(const function_application_exprt &f)
Integer value represented by a string.
nonstd::optional< T > optionalt
Definition: optional.h:35
exprt add_axioms_for_is_suffix(const function_application_exprt &f, bool swap_arguments=false)
Test if the target is a suffix of the string.
exprt add_axioms_for_last_index_of_string(const array_string_exprt &haystack, const array_string_exprt &needle, const exprt &from_index)
Add axioms stating that the returned value is the index within haystack of the last occurrence of nee...
TO_BE_DOCUMENTED.
Definition: namespace.h:74
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 ...
exprt add_axioms_for_string_of_int(const array_string_exprt &res, const exprt &input_int, size_t max_size=0)
Add axioms enforcing that the string corresponds to the result of String.valueOf(I) or String...
exprt add_axioms_for_set_length(const function_application_exprt &f)
Reduce or extend a string to have the given length.
exprt add_axioms_for_equals_ignore_case(const function_application_exprt &f)
Equality of the content ignoring case of characters.
The plus expression.
Definition: std_expr.h:893
exprt add_axioms_for_char_literal(const function_application_exprt &f)
add axioms stating that the returned value is equal to the argument
symbol_exprt operator()(const irep_idt &prefix, const typet &type=bool_typet())
generate a new symbol expression of the given type with some prefix
bitvector_typet index_type()
Definition: c_types.cpp:16
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
array_string_exprt make_char_array_for_char_pointer(const exprt &char_pointer, const typet &char_array_type)
exprt add_axioms_for_char_set(const function_application_exprt &f)
Set a character to a specific value at an index of the string.
static exprt is_low_surrogate(const exprt &chr)
the output is true when the character is a low surrogate for UTF-16 encoding, see https://en...
array_string_exprt of_argument(const exprt &arg)
Converts a struct containing a length and pointer to an array.
exprt add_axioms_for_insert_double(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(D) java function
exprt add_axioms_for_concat_substr(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 â...
exprt add_axioms_for_insert_int(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(I) java function
exprt length_constraint_for_concat_substr(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 the length of res is that of the concatenation of s1 with the substring of ...
const std::unordered_map< exprt, array_string_exprt, irep_hash > & get_arrays_of_pointers() const
std::vector< exprt > operandst
Definition: expr.h:45
unsigned long to_integer_or_default(const exprt &expr, unsigned long def)
If the expression is a constant expression then we get the value of it as an unsigned long...
exprt maximum(const exprt &a, const exprt &b)
#define DEPRECATED(msg)
Definition: deprecate.h:23
void insert(const exprt &pointer_expr, array_string_exprt &array)
String expressions for the string solver.
static constant_exprt constant_char(int i, const typet &char_type)
generate constant character expression with character type.
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
symbol_exprt fresh_exist_index(const irep_idt &prefix, const typet &type)
generate an index symbol which is existentially quantified
exprt get_numeric_value_from_character(const exprt &chr, const typet &char_type, const typet &type, const bool strict_formatting, unsigned long radix_ul)
Get the numeric value of a character, assuming that the radix is large enough.
exprt 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...
exprt add_axioms_for_char_at(const function_application_exprt &f)
Character at a given position.
exprt 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...
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...
void 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.
Base class for all expressions.
Definition: expr.h:42
optionalt< exprt > make_array_pointer_association(const function_application_exprt &expr)
Associate array to pointer, and array to length.
exprt 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 ...
exprt 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...
exprt add_axioms_for_set_char(const array_string_exprt &res, const array_string_exprt &str, const exprt &position, const exprt &character)
Add axioms ensuring that the result res is similar to input string str where the character at index p...
size_t max_printed_string_length(const typet &type, unsigned long ul_radix)
Calculate the string length needed to represent any value of the given type using the given radix...
exprt add_axioms_from_bool(const function_application_exprt &f)
Add axioms corresponding to the String.valueOf(Z) java function.
exprt add_axioms_for_string_of_float(const function_application_exprt &f)
String representation of a float value.
exprt add_axioms_for_format(const function_application_exprt &f)
Formatted string using a format string and list of arguments.
std::set< array_string_exprt > created_strings
Universally quantified string constraint
exprt add_axioms_for_code_point_before(const function_application_exprt &f)
add axioms corresponding to the String.codePointBefore java function
static exprt character_equals_ignore_case(exprt char1, exprt char2, exprt char_a, exprt char_A, exprt char_Z)
Returns an expression which is true when the two given characters are equal when ignoring case for AS...
exprt sum_overflows(const plus_exprt &sum)
exprt add_axioms_for_constrain_characters(const function_application_exprt &f)
Add axioms to ensure all characters of a string belong to a given set.
exprt add_axioms_for_cprover_string(const array_string_exprt &res, const exprt &arg, const exprt &guard)
Convert an expression of type string_typet to a string_exprt.
Expression to hold a symbol (variable)
Definition: std_expr.h:90
int8_t s1
Definition: bytecode_info.h:59
exprt add_axioms_for_fractional_part(const array_string_exprt &res, const exprt &i, size_t max_size)
Add axioms for representing the fractional part of a floating point starting with a dot...
int16_t s2
Definition: bytecode_info.h:60
exprt add_axioms_for_insert_bool(const function_application_exprt &f)
add axioms corresponding to the StringBuilder.insert(Z) java function
std::string utf16_constant_array_to_java(const array_exprt &arr, std::size_t length)
Construct a string from a constant array.
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.
std::vector< string_constraintt > constraints
std::map< string_not_contains_constraintt, symbol_exprt > witness
std::unordered_map< array_string_exprt, symbol_exprt, irep_hash > length_of_array
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_for_concat_char(const array_string_exprt &res, const array_string_exprt &s1, const exprt &c)
Add axioms enforcing that res is the concatenation of s1 with character c.
exprt add_axioms_from_char(const function_application_exprt &f)
Conversion from char to string.
const std::vector< symbol_exprt > & get_index_symbols() const
Symbols used in existential quantifications.
struct constructor from list of elements
Definition: std_expr.h:1815
static exprt int_of_hex_char(const exprt &chr)
Returns the integer value represented by the character.
static exprt is_high_surrogate(const exprt &chr)
the output is true when the character is a high surrogate for UTF-16 encoding, see https://en...
bitvector_typet char_type()
Definition: c_types.cpp:114
exprt add_axioms_for_concat(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.
exprt add_axioms_for_concat_code_point(const function_application_exprt &f)
Add axioms corresponding to the StringBuilder.appendCodePoint(I) function.
array constructor from list of elements
Definition: std_expr.h:1617
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.
exprt 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 ...
symbol_generatort & fresh_symbol
array index operator
Definition: std_expr.h:1462
exprt axiom_for_is_positive_index(const exprt &x)
expression true exactly when the index is positive
array_string_exprt add_axioms_for_format_specifier(const format_specifiert &fs, const struct_exprt &arg, const typet &index_type, const typet &char_type)
Parse s and add axioms ensuring the output corresponds to the output of String.format.