cprover
string_constraint_generatort Class Referencefinal

#include <string_constraint_generator.h>

Collaboration diagram for string_constraint_generatort:
[legend]

Classes

class  format_specifiert
 

Public Member Functions

 string_constraint_generatort (const namespacet &ns)
 
const std::vector< exprt > & get_lemmas () const
 Axioms are of three kinds: universally quantified string constraint, not contains string constraints and simple formulas. More...
 
void add_lemma (const exprt &)
 
const std::vector< string_constraintt > & get_constraints () const
 
const std::vector< string_not_contains_constraintt > & get_not_contains_constraints () const
 
void clear_constraints ()
 Clear all constraints and lemmas. More...
 
const std::vector< symbol_exprt > & get_boolean_symbols () const
 Boolean symbols for the results of some string functions. More...
 
const std::vector< symbol_exprt > & get_index_symbols () const
 Symbols used in existential quantifications. More...
 
const std::set< array_string_exprt > & get_created_strings () const
 Set of strings that have been created by the generator. More...
 
exprt get_witness_of (const string_not_contains_constraintt &c, const exprt &univ_val) const
 
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. More...
 
symbol_exprt fresh_univ_index (const irep_idt &prefix, const typet &type)
 generate an index symbol to be used as an universaly quantified variable More...
 
symbol_exprt fresh_exist_index (const irep_idt &prefix, const typet &type)
 generate an index symbol which is existentially quantified More...
 
optionalt< exprtmake_array_pointer_association (const function_application_exprt &expr)
 Associate array to pointer, and array to length. More...
 
const signedbv_typet get_return_code_type ()
 
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. More...
 
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. More...
 
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 ‘start_index’and ending at indexend_index'`. More...
 
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. More...
 

Public Attributes

symbol_generatort fresh_symbol
 
array_poolt array_pool
 
std::map< string_not_contains_constraintt, symbol_exprtwitness
 

Private Member Functions

symbol_exprt fresh_boolean (const irep_idt &prefix)
 generate a Boolean symbol which is existentially quantified More...
 
array_string_exprt fresh_string (const typet &index_type, const typet &char_type)
 construct a string expression whose length and content are new variables More...
 
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 symbol. More...
 
const array_string_exprtchar_array_of_pointer (const exprt &pointer, const exprt &length)
 Adds creates a new array if it does not already exists. More...
 
exprt axiom_for_is_positive_index (const exprt &x)
 expression true exactly when the index is positive More...
 
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. More...
 
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. More...
 
exprt add_axioms_for_char_at (const function_application_exprt &f)
 Character at a given position. More...
 
exprt add_axioms_for_code_point_at (const function_application_exprt &f)
 add axioms corresponding to the String.codePointAt java function More...
 
exprt add_axioms_for_code_point_before (const function_application_exprt &f)
 add axioms corresponding to the String.codePointBefore java function More...
 
exprt add_axioms_for_contains (const function_application_exprt &f)
 Test whether a string contains another. More...
 
exprt add_axioms_for_equals (const function_application_exprt &f)
 Equality of the content of two strings. More...
 
exprt add_axioms_for_equals_ignore_case (const function_application_exprt &f)
 Equality of the content ignoring case of characters. More...
 
exprt add_axioms_for_hash_code (const function_application_exprt &f)
 Value that is identical for strings with the same content. More...
 
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. More...
 
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 to 0 and the first string is a prefix of the second one, starting at position offset. More...
 
exprt add_axioms_for_is_prefix (const function_application_exprt &f, bool swap_arguments=false)
 Test if the target is a prefix of the string. More...
 
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. More...
 
exprt add_axioms_for_length (const function_application_exprt &f)
 Length of a string. More...
 
exprt add_axioms_for_empty_string (const function_application_exprt &f)
 Add axioms to say that the returned string expression is empty. More...
 
exprt add_axioms_for_char_set (const function_application_exprt &f)
 Set a character to a specific value at an index of the string. More...
 
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 application More...
 
exprt add_axioms_for_concat_char (const function_application_exprt &f)
 Add axioms enforcing that the string represented by the two first expressions is equal to the concatenation of the string argument and the character argument of the function application. More...
 
exprt add_axioms_for_concat (const function_application_exprt &f)
 String concatenation. More...
 
exprt add_axioms_for_concat_code_point (const function_application_exprt &f)
 Add axioms corresponding to the StringBuilder.appendCodePoint(I) function. More...
 
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. More...
 
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 positions start (included) and end (not included). More...
 
exprt add_axioms_for_delete (const function_application_exprt &f)
 Remove a portion of a string. More...
 
exprt add_axioms_for_delete_char_at (const function_application_exprt &expr)
 add axioms corresponding to the StringBuilder.deleteCharAt java function More...
 
exprt add_axioms_for_format (const function_application_exprt &f)
 Formatted string using a format string and list of arguments. More...
 
exprt add_axioms_for_format (const array_string_exprt &res, const std::string &s, const exprt::operandst &args)
 Parse s and add axioms ensuring the output corresponds to the output of String.format. More...
 
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. More...
 
exprt add_axioms_for_insert (const function_application_exprt &f)
 Insertion of a string in another at a specific index. More...
 
exprt add_axioms_for_insert_int (const function_application_exprt &f)
 add axioms corresponding to the StringBuilder.insert(I) java function More...
 
exprt add_axioms_for_insert_bool (const function_application_exprt &f)
 add axioms corresponding to the StringBuilder.insert(Z) java function More...
 
exprt add_axioms_for_insert_char (const function_application_exprt &f)
 Add axioms corresponding to the StringBuilder.insert(C) java function. More...
 
exprt add_axioms_for_insert_float (const function_application_exprt &f)
 Add axioms corresponding to the StringBuilder.insert(F) java function. More...
 
exprt add_axioms_for_insert_double (const function_application_exprt &f)
 add axioms corresponding to the StringBuilder.insert(D) java function More...
 
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. More...
 
exprt add_axioms_from_literal (const function_application_exprt &f)
 String corresponding to an internal cprover string. More...
 
exprt add_axioms_from_int (const function_application_exprt &f)
 Convert an integer to a string. More...
 
exprt add_axioms_from_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.valueOf(J) Java functions applied on the integer expression. More...
 
exprt add_axioms_from_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.valueOf(JI) Java functions applied on the integer expression. More...
 
exprt 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. More...
 
exprt add_axioms_from_int_hex (const function_application_exprt &f)
 Add axioms corresponding to the Integer.toHexString(I) java function. More...
 
exprt add_axioms_from_long (const function_application_exprt &f)
 Add axioms corresponding to the String.valueOf(J) java function. More...
 
exprt add_axioms_from_bool (const function_application_exprt &f)
 Add axioms corresponding to the String.valueOf(Z) java function. More...
 
exprt add_axioms_from_bool (const array_string_exprt &res, const exprt &i)
 Add axioms stating that the returned string equals "true" when the Boolean expression is true and "false" when it is false. More...
 
exprt add_axioms_from_char (const function_application_exprt &f)
 Conversion from char to string. More...
 
exprt add_axioms_from_char (const array_string_exprt &res, const exprt &i)
 Add axiom stating that string res has length 1 and the character it contains equals c. More...
 
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 of needle (c) starting the search at from_index, or is -1 if no such character occurs at or after position from_index. More...
 
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 of needle starting the search at from_index, or -1 if needle does not occur at or after position from_index. More...
 
exprt add_axioms_for_index_of (const function_application_exprt &f)
 Index of the first occurence of a target inside the string. More...
 
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 needle starting the search backward at from_index (ie the index is smaller or equal to from_index), or -1 if needle does not occur before from_index. More...
 
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 of needle (c) starting the search backward at from_index, or -1 if no such character occurs at or before position from_index. More...
 
exprt add_axioms_for_last_index_of (const function_application_exprt &f)
 Index of the last occurence of a target inside the string. More...
 
exprt add_axioms_for_string_of_float (const function_application_exprt &f)
 String representation of a float value. More...
 
exprt add_axioms_for_string_of_float (const array_string_exprt &res, const exprt &f)
 Add axioms corresponding to the integer part of m, in decimal form with no leading zeroes, followed by '. More...
 
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. More...
 
exprt add_axioms_from_float_scientific_notation (const array_string_exprt &res, const exprt &f)
 Add axioms to write the float in scientific notation. More...
 
exprt add_axioms_from_float_scientific_notation (const function_application_exprt &f)
 Representation of a float value in scientific notation. More...
 
exprt add_axioms_from_double (const function_application_exprt &f)
 Add axioms corresponding to the String.valueOf(D) java function. More...
 
exprt add_axioms_for_replace (const function_application_exprt &f)
 Replace a character by another in a string. More...
 
exprt add_axioms_for_set_length (const function_application_exprt &f)
 Reduce or extend a string to have the given length. More...
 
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(start, 0)and end' = max(min(end, |str|), start')`. More...
 
exprt add_axioms_for_substring (const function_application_exprt &f)
 Substring of a string between two indices. More...
 
exprt add_axioms_for_to_lower_case (const function_application_exprt &f)
 Conversion of a string to lower case. More...
 
exprt add_axioms_for_to_upper_case (const function_application_exprt &f)
 Conversion of a string to upper case. More...
 
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 have been converted to uppercase. More...
 
exprt add_axioms_for_trim (const function_application_exprt &f)
 Remove leading and trailing whitespaces. More...
 
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 More...
 
exprt add_axioms_for_char_literal (const function_application_exprt &f)
 add axioms stating that the returned value is equal to the argument More...
 
exprt add_axioms_for_code_point_count (const function_application_exprt &f)
 Add axioms corresponding the String.codePointCount java function. More...
 
exprt add_axioms_for_offset_by_code_point (const function_application_exprt &f)
 Add axioms corresponding the String.offsetByCodePointCount java function. More...
 
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. More...
 
void add_axioms_for_correct_number_format (const exprt &input_int, 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. More...
 
exprt add_axioms_for_parse_int (const function_application_exprt &f)
 Integer value represented by a string. More...
 
exprt add_axioms_for_compare_to (const function_application_exprt &f)
 Lexicographic comparison of two strings. More...
 
symbol_exprt add_axioms_for_intern (const function_application_exprt &f)
 Add axioms corresponding to the String.intern java function. More...
 
exprt associate_array_to_pointer (const function_application_exprt &f)
 Associate a char array to a char pointer. More...
 
exprt associate_length_to_array (const function_application_exprt &f)
 Associate an integer length to a char array. More...
 
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. More...
 

Static Private Member Functions

static constant_exprt constant_char (int i, const typet &char_type)
 generate constant character expression with character type. More...
 
static exprt int_of_hex_char (const exprt &chr)
 Returns the integer value represented by the character. More...
 
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.wikipedia.org/wiki/UTF-16 for more explenation about the encoding; this is true when the character is in the range 0xD800..0xDBFF More...
 
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.wikipedia.org/wiki/UTF-16 for more explenation about the encoding; this is true when the character is in the range 0xDC00..0xDFFF More...
 
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 ASCII. More...
 

Private Attributes

std::set< array_string_exprtcreated_strings
 
const messaget message
 
std::vector< exprtlemmas
 
std::vector< string_constrainttconstraints
 
std::vector< string_not_contains_constrainttnot_contains_constraints
 
std::vector< symbol_exprtboolean_symbols
 
std::vector< symbol_exprtindex_symbols
 
const namespacet ns
 
std::map< array_string_exprt, exprthash_code_of_string
 
std::map< array_string_exprt, symbol_exprtintern_of_string
 

Detailed Description

Definition at line 87 of file string_constraint_generator.h.

Constructor & Destructor Documentation

◆ string_constraint_generatort()

string_constraint_generatort::string_constraint_generatort ( const namespacet ns)
explicit

Definition at line 31 of file string_constraint_generator_main.cpp.

Member Function Documentation

◆ add_axioms_for_char_at()

exprt string_constraint_generatort::add_axioms_for_char_at ( const function_application_exprt f)
private

Character at a given position.

Add axioms stating that the character of the string at position given by second argument is equal to the returned value. This axiom is \( char = str[i] \).

Parameters
ffunction application with arguments string str and integer i
Returns
character expression char

Definition at line 611 of file string_constraint_generator_main.cpp.

References function_application_exprt::arguments(), fresh_symbol, get_string_expr(), lemmas, and PRECONDITION.

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_char_literal()

exprt string_constraint_generatort::add_axioms_for_char_literal ( const function_application_exprt f)
private

add axioms stating that the returned value is equal to the argument

Parameters
ffunction application with one character argument
Returns
a new character expression

Definition at line 576 of file string_constraint_generator_main.cpp.

References function_application_exprt::arguments(), CHECK_RETURN, from_integer(), string_constantt::get_value(), PRECONDITION, to_string_constant(), and UNIMPLEMENTED.

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_char_set()

exprt string_constraint_generatort::add_axioms_for_char_set ( const function_application_exprt f)
private

Set a character to a specific value at an index of the string.

Add axioms ensuring that the result res is similar to input string str where the character at index pos is set to char. These axioms are:

  1. \( |{\tt res}| = |{\tt str}|\)
  2. \( {\tt res}[{\tt pos}]={\tt char}\)
  3. \( \forall i < min(|{\tt res}|, pos). {\tt res}[i] = {\tt str}[i]\)
  4. \( \forall pos+1 <= i < |{\tt res}|.\ {\tt res}[i] = {\tt str}[i]\)
    Parameters
    ffunction application with arguments integer |res|, character pointer &res[0], refined_string str, integer pos, and character char
    Returns
    an integer expression which is 1 when pos is out of bounds and 0 otherwise

Definition at line 391 of file string_constraint_generator_transformation.cpp.

References function_application_exprt::arguments(), char_array_of_pointer(), constraints, fresh_univ_index(), from_integer(), get_string_expr(), lemmas, minimum(), PRECONDITION, and exprt::type().

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_characters_in_integer_string()

void string_constraint_generatort::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 
)
private

Add axioms connecting the characters in the input string to the value of the output integer.

It is constructive because it gives a formula for input_int in terms of the characters in str.

Parameters
input_intthe integer represented by str
typethe type for input_int
strict_formattingif true, don't allow a leading plus, redundant zeros or upper case letters
strinput string
max_string_lengththe maximum length str can have
radixthe radix, with the same type as input_int
radix_ulthe radix as an unsigned long, or 0 if that can't be determined

Deal with size==1 case separately. There are axioms from add_axioms_for_correct_number_format which say that the string must contain at least one digit, so we don't have to worry about "+" or "-".

Definition at line 404 of file string_constraint_generator_valueof.cpp.

References string_exprt< child_t >::axiom_for_has_length(), char_type(), conjunction(), constant_char(), array_string_exprt::content(), from_integer(), get_numeric_value_from_character(), lemmas, typet::subtype(), and exprt::type().

Referenced by add_axioms_for_parse_int(), and add_axioms_from_int_with_radix().

◆ add_axioms_for_code_point()

exprt string_constraint_generatort::add_axioms_for_code_point ( const array_string_exprt res,
const exprt code_point 
)
private

add axioms for the conversion of an integer representing a java code point to a utf-16 string

Parameters
resarray of characters corresponding to the result fo the function
code_pointan expression representing a java code point
Returns
integer expression equal to zero

Definition at line 20 of file string_constraint_generator_code_points.cpp.

References string_exprt< child_t >::axiom_for_has_length(), char_type(), array_string_exprt::content(), from_integer(), get_return_code_type(), irept::id(), lemmas, PRECONDITION, typet::subtype(), and exprt::type().

Referenced by add_axioms_for_concat_code_point().

◆ add_axioms_for_code_point_at()

exprt string_constraint_generatort::add_axioms_for_code_point_at ( const function_application_exprt f)
private

add axioms corresponding to the String.codePointAt java function

Parameters
ffunction application with arguments a string and an index
Returns
a integer expression corresponding to a code point

Definition at line 119 of file string_constraint_generator_code_points.cpp.

References function_application_exprt::arguments(), fresh_symbol, from_integer(), get_string_expr(), irept::id(), is_high_surrogate(), is_low_surrogate(), lemmas, pair_value(), pos(), PRECONDITION, and exprt::type().

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_code_point_before()

exprt string_constraint_generatort::add_axioms_for_code_point_before ( const function_application_exprt f)
private

add axioms corresponding to the String.codePointBefore java function

parameters: function application with two arguments: a string and an
index
Returns
a integer expression corresponding to a code point

Definition at line 148 of file string_constraint_generator_code_points.cpp.

References function_application_exprt::arguments(), fresh_symbol, from_integer(), get_string_expr(), is_high_surrogate(), is_low_surrogate(), lemmas, array_string_exprt::length(), pair_value(), PRECONDITION, and exprt::type().

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_code_point_count()

exprt string_constraint_generatort::add_axioms_for_code_point_count ( const function_application_exprt f)
private

Add axioms corresponding the String.codePointCount java function.

add axioms giving approximate bounds on the result of the String.codePointCount java function

Deprecated:
This is Java specific and should be implemented in Java.
Parameters
ffunction application with three arguments string str, integer begin and integer end.
Returns
an integer expression

Definition at line 180 of file string_constraint_generator_code_points.cpp.

References function_application_exprt::arguments(), fresh_symbol, from_integer(), get_string_expr(), lemmas, minimum(), PRECONDITION, and exprt::type().

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_compare_to()

exprt string_constraint_generatort::add_axioms_for_compare_to ( const function_application_exprt f)
private

Lexicographic comparison of two strings.

Add axioms ensuring the result corresponds to that of the String.compareTo Java function. In the lexicographic comparison, x representing the first point where the two strings differ, we add axioms:

  • \( res=0 \Rightarrow |s1|=|s2|\)
  • \( \forall i<|s1|. s1[i]=s2[i] \)
  • \( \exists x.\ res\ne 0 \Rightarrow x > 0 \land ((|s1| \ge |s2| \land x<|s1|) \lor (|s1| \ge |s2| \land x<|s2|) \land res=s1[x]-s2[x] ) \lor cond2: (|s1|<|s2| \land x=|s1|) \lor (|s1| > |s2| \land x=|s2|) \land res=|s1|-|s2|) \)
  • \( \forall i'<x. res\ne 0 \Rightarrow s1[i]=s2[i] \)
    Parameters
    ffunction application with arguments refined_string s1 and refined_string s2
    Returns
    integer expression res

Definition at line 212 of file string_constraint_generator_comparison.cpp.

References function_application_exprt::arguments(), constraints, fresh_exist_index(), fresh_symbol, fresh_univ_index(), from_integer(), get_string_expr(), index_type(), lemmas, PRECONDITION, and exprt::type().

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_concat() [1/2]

exprt string_constraint_generatort::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.

Deprecated:
should use concat_substr instead
Parameters
resstring_expression corresponding to the result
s1the string expression to append to
s2the string expression to append to the first one
Returns
an integer expression

Definition at line 151 of file string_constraint_generator_concat.cpp.

References add_axioms_for_concat_substr(), and from_integer().

Referenced by add_axioms_for_concat(), add_axioms_for_concat_code_point(), add_axioms_for_delete(), add_axioms_for_format(), add_axioms_for_function_application(), add_axioms_for_string_of_float(), add_axioms_from_float_scientific_notation(), and string_concatenation_builtin_functiont::add_constraints().

◆ add_axioms_for_concat() [2/2]

exprt string_constraint_generatort::add_axioms_for_concat ( const function_application_exprt f)
private

String concatenation.

This primitive accepts 4 or 6 arguments. Add axioms enforcing that res is the concatenation of s1 with the substring of s2 starting at index ‘start_index’and ending at indexend_index'`. (More...)

Parameters
ffunction application with arguments integer |res|, character pointer &res[0], refined_string s1, refined_string s2, optional integer start_index, optional integer end_index
Returns
an integer expression

Definition at line 171 of file string_constraint_generator_concat.cpp.

References add_axioms_for_concat(), add_axioms_for_concat_substr(), function_application_exprt::arguments(), char_array_of_pointer(), get_string_expr(), and PRECONDITION.

◆ add_axioms_for_concat_char() [1/2]

exprt string_constraint_generatort::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.

These axioms are :

  • \( |res|=|s1|+1 \)
  • \( \forall i<|s1|. res[i]=s1[i] \)
  • \( res[|s1|]=c \)
Parameters
resstring expression
s1string expression
ccharacter expression
Returns
code 0 on success

Definition at line 114 of file string_constraint_generator_concat.cpp.

References constraints, fresh_univ_index(), from_integer(), get_return_code_type(), index_type(), lemmas, array_string_exprt::length(), length_constraint_for_concat_char(), and exprt::type().

Referenced by add_axioms_for_concat_char(), add_axioms_for_function_application(), and string_concat_char_builtin_functiont::add_constraints().

◆ add_axioms_for_concat_char() [2/2]

exprt string_constraint_generatort::add_axioms_for_concat_char ( const function_application_exprt f)
private

Add axioms enforcing that the string represented by the two first expressions is equal to the concatenation of the string argument and the character argument of the function application.

Parameters
ffunction application with a length, pointer, string and character argument.
Returns
code 0 on success

Definition at line 192 of file string_constraint_generator_concat.cpp.

References add_axioms_for_concat_char(), function_application_exprt::arguments(), char_array_of_pointer(), get_string_expr(), and PRECONDITION.

◆ add_axioms_for_concat_code_point()

exprt string_constraint_generatort::add_axioms_for_concat_code_point ( const function_application_exprt f)
private

Add axioms corresponding to the StringBuilder.appendCodePoint(I) function.

Deprecated:
java specific
Parameters
ffunction application with two arguments: a string and a code point
Returns
an expression

Definition at line 207 of file string_constraint_generator_concat.cpp.

References add_axioms_for_code_point(), add_axioms_for_concat(), function_application_exprt::arguments(), char_array_of_pointer(), char_type(), fresh_string(), get_string_expr(), index_type(), PRECONDITION, and typet::subtype().

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_concat_substr()

exprt string_constraint_generatort::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 ‘start_index’and ending at indexend_index'`.

Where start_index' is max(0, start_index) and end_index' is max(min(end_index, s2.length), start_index') If s1.length + end_index' - start_index' is greater than the maximal integer of the type of res.length, then the result gets truncated to the size of this maximal integer.

These axioms are:

  1. \(|res| = overflow ? |s_1| + end\_index' - start\_index' : max_int \)
  2. \(\forall i<|s_1|. res[i]=s_1[i] \)
  3. \(\forall i< |res| - |s_1|.\ res[i+|s_1|] = s_2[start\_index'+i]\)
Parameters
resan array of characters expression
s1an array of characters expression
s2an array of characters expression
start_indexinteger expression
end_indexinteger expression
Returns
integer expression 0

Definition at line 37 of file string_constraint_generator_concat.cpp.

References constraints, fresh_univ_index(), from_integer(), get_return_code_type(), index_type(), lemmas, array_string_exprt::length(), length_constraint_for_concat_substr(), maximum(), minimum(), and exprt::type().

Referenced by add_axioms_for_concat(), and string_concatenation_builtin_functiont::add_constraints().

◆ add_axioms_for_constant()

exprt string_constraint_generatort::add_axioms_for_constant ( const array_string_exprt res,
irep_idt  sval,
const exprt guard = true_exprt() 
)
private

Add axioms ensuring that the provided string expression and constant are equal.

Parameters
resarray of characters for the result
svala string constant
guardcondition under which the axiom should apply, true by default
Returns
integer expression equal to zero

Definition at line 24 of file string_constraint_generator_constants.cpp.

References char_type(), array_string_exprt::content(), from_integer(), get_return_code_type(), id2string(), index_type(), lemmas, array_string_exprt::length(), typet::subtype(), exprt::type(), utf8_to_utf16_little_endian(), and widen().

Referenced by add_axioms_for_cprover_string(), add_axioms_for_format(), add_axioms_for_format_specifier(), and add_axioms_from_float_scientific_notation().

◆ add_axioms_for_constrain_characters()

exprt string_constraint_generatort::add_axioms_for_constrain_characters ( const function_application_exprt f)
private

Add axioms to ensure all characters of a string belong to a given set.

The axiom is: \(\forall i \in [start, end).\ s[i] \in char_set \), where char_set is given by the string char_set_string composed of three characters low_char, - and high_char. Character c belongs to char_set if \(low_char \le c \le high_char\).

Parameters
fa function application with arguments: integer |s|, character pointer &s[0], string char_set_string, optional integers start and end
Returns
integer expression whose value is zero

Definition at line 341 of file string_constraint_generator_main.cpp.

References add_constraint_on_characters(), function_application_exprt::arguments(), dstringt::c_str(), char_array_of_pointer(), from_integer(), get_return_code_type(), constant_exprt::get_value(), array_string_exprt::length(), PRECONDITION, to_constant_expr(), and exprt::type().

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_contains()

exprt string_constraint_generatort::add_axioms_for_contains ( const function_application_exprt f)
private

Test whether a string contains another.

Add axioms ensuring the returned value is true when the first string contains the second. These axioms are:

  1. \( contains \Rightarrow |s_0| \ge |s_1| \)
  2. \( contains \Rightarrow 0 \le startpos \le |s_0|-|s_1| \)
  3. \( !contains \Rightarrow startpos = -1 \)
  4. \( \forall qvar < |s_1|.\ contains \Rightarrow s_1[qvar] = s_0[startpos + qvar] \)
  5. \( \forall startpos \le |s_0|-|s_1|. \ (!contains \land |s_0| \ge |s_1|) \Rightarrow \exists witness < |s_1|. \ s_1[witness] \ne s_0[startpos+witness] \)
    Warning
    slow for target longer than one character
    Parameters
    ffunction application with arguments refined_string s0 refined_string s1
    Returns
    Boolean expression contains

Definition at line 207 of file string_constraint_generator_testing.cpp.

References function_application_exprt::arguments(), axiom_for_is_positive_index(), constraints, fresh_boolean(), fresh_exist_index(), fresh_univ_index(), from_integer(), get_string_expr(), irept::id(), index_type(), lemmas, not_contains_constraints, PRECONDITION, and exprt::type().

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_copy()

exprt string_constraint_generatort::add_axioms_for_copy ( const function_application_exprt f)
private

add axioms to say that the returned string expression is equal to the argument of the function application

Deprecated:
should use substring instead
Parameters
ffunction application with one argument, which is a string, or three arguments: string, integer offset and count
Returns
a new string expression

Definition at line 539 of file string_constraint_generator_main.cpp.

References from_integer(), index_type(), array_string_exprt::length(), PRECONDITION, and exprt::type().

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_correct_number_format()

void string_constraint_generatort::add_axioms_for_correct_number_format ( const exprt input_int,
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 
)
private

Add axioms making the return value true if the given string is a correct number in the given radix.

Parameters
input_intthe number being represented as a string
strstring expression
radix_as_charthe radix as an expression of the same type as the characters in str
radix_ulthe radix, which should be between 2 and 36, or 0, in which case the return value will work for any radix
max_sizemaximum number of characters
strict_formattingif true, don't allow a leading plus, redundant zeros or upper case letters

index < length => is_digit_with_radix(str[index], radix)

Definition at line 318 of file string_constraint_generator_valueof.cpp.

References string_exprt< child_t >::axiom_for_has_length(), string_exprt< child_t >::axiom_for_length_ge(), string_exprt< child_t >::axiom_for_length_le(), char_type(), constant_char(), array_string_exprt::content(), from_integer(), index_type(), is_digit_with_radix(), lemmas, array_string_exprt::length(), typet::subtype(), and exprt::type().

Referenced by add_axioms_for_parse_int(), and add_axioms_from_int_with_radix().

◆ add_axioms_for_cprover_string()

exprt string_constraint_generatort::add_axioms_for_cprover_string ( const array_string_exprt res,
const exprt arg,
const exprt guard 
)
private

Convert an expression of type string_typet to a string_exprt.

Parameters
resstring expression for the result
argexpression of type string typet
guardcondition under which res should be equal to arg
Returns
0 if constraints were added, 1 if expression could not be handled and no constraint was added. Expression we can handle are of the form \( e := "<string constant>" | (expr)? e : e \)

Definition at line 77 of file string_constraint_generator_constants.cpp.

References add_axioms_for_constant(), from_integer(), and get_return_code_type().

Referenced by add_axioms_from_literal().

◆ add_axioms_for_delete() [1/2]

exprt string_constraint_generatort::add_axioms_for_delete ( const array_string_exprt res,
const array_string_exprt str,
const exprt start,
const exprt end 
)
private

Add axioms stating that res corresponds to the input str where we removed characters between the positions start (included) and end (not included).

These axioms are the same as would be generated for: concat(substring(str, 0, start), substring(end, |str|)) (see add_axioms_for_substring and add_axioms_for_concat_substr).

Parameters
resarray of characters expression
strarray of characters expression
startinteger expression
endinteger expression
Returns
integer expression different from zero to signal an exception

Definition at line 529 of file string_constraint_generator_transformation.cpp.

References add_axioms_for_concat(), add_axioms_for_substring(), char_type(), array_string_exprt::content(), fresh_string(), from_integer(), index_type(), array_string_exprt::length(), PRECONDITION, typet::subtype(), and exprt::type().

Referenced by add_axioms_for_delete(), add_axioms_for_delete_char_at(), and add_axioms_for_function_application().

◆ add_axioms_for_delete() [2/2]

exprt string_constraint_generatort::add_axioms_for_delete ( const function_application_exprt f)
private

Remove a portion of a string.

Add axioms stating that res corresponds to the input str where we removed characters between the positions start (included) and end (not included). (More...)

Parameters
ffunction application with arguments integer |res|, character pointer &res[0], refined_string str, integer start and integer end
Returns
an integer expression whose value is different from 0 to signal an exception

Definition at line 561 of file string_constraint_generator_transformation.cpp.

References add_axioms_for_delete(), function_application_exprt::arguments(), char_array_of_pointer(), get_string_expr(), and PRECONDITION.

◆ add_axioms_for_delete_char_at()

exprt string_constraint_generatort::add_axioms_for_delete_char_at ( const function_application_exprt f)
private

add axioms corresponding to the StringBuilder.deleteCharAt java function

Parameters
ffunction application with two arguments, the first is a string and the second is an index
Returns
an expression whose value is non null to signal an exception

Definition at line 503 of file string_constraint_generator_transformation.cpp.

References add_axioms_for_delete(), function_application_exprt::arguments(), char_array_of_pointer(), from_integer(), get_string_expr(), and PRECONDITION.

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_empty_string()

exprt string_constraint_generatort::add_axioms_for_empty_string ( const function_application_exprt f)
private

Add axioms to say that the returned string expression is empty.

Parameters
ffunction application with arguments integer length and character pointer ptr.
Returns
integer expression equal to zero

Definition at line 61 of file string_constraint_generator_constants.cpp.

References function_application_exprt::arguments(), from_integer(), get_return_code_type(), lemmas, and PRECONDITION.

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_equals()

exprt string_constraint_generatort::add_axioms_for_equals ( const function_application_exprt f)
private

Equality of the content of two strings.

Add axioms stating that the result is true exactly when the strings represented by the arguments are equal. These axioms are:

  1. \( eq \Rightarrow |s_1|=|s_2|\)
  2. \( \forall i<|s_1|.\ eq \Rightarrow s_1[i]=s_2[i] \)
  3. \( \lnot eq \Rightarrow (|s_1| \ne |s_2| \land witness=-1) \lor (0 \le witness<|s_1| \land s_1[witness] \ne s_2[witness]) \)
    Parameters
    ffunction application with arguments refined_string s1 and refined_string s2
    Returns
    Boolean expression eq

Definition at line 29 of file string_constraint_generator_comparison.cpp.

References function_application_exprt::arguments(), constraints, fresh_boolean(), fresh_exist_index(), fresh_univ_index(), from_integer(), get_string_expr(), irept::id(), index_type(), lemmas, PRECONDITION, exprt::type(), and witness.

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_equals_ignore_case()

exprt string_constraint_generatort::add_axioms_for_equals_ignore_case ( const function_application_exprt f)
private

Equality of the content ignoring case of characters.

Add axioms ensuring the result is true when the two strings are equal if case is ignored. These axioms are:

  1. \( eq \Rightarrow |s_1|=|s_2|\)
  2. \( \forall i \in [0, |s_1|). \ eq \Rightarrow {\tt equal\_ignore\_case}(s_1[i],s_2[i]) \)
  3. \( \lnot eq \Rightarrow |s_1| \ne |s_2| \lor (0 \le witness<|s_1| \land\lnot {\tt equal\_ignore\_case}(s_1[witness],s_2[witness]) \)
    Parameters
    ffunction application with arguments refined_string s1 and refined_string s2
    Returns
    Boolean expression eq

Definition at line 114 of file string_constraint_generator_comparison.cpp.

References function_application_exprt::arguments(), char_type(), character_equals_ignore_case(), constant_char(), constraints, fresh_boolean(), fresh_exist_index(), fresh_univ_index(), from_integer(), get_string_expr(), irept::id(), index_type(), lemmas, PRECONDITION, typet::subtype(), exprt::type(), and witness.

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_format() [1/2]

exprt string_constraint_generatort::add_axioms_for_format ( const function_application_exprt f)
private

Formatted string using a format string and list of arguments.

Add axioms to specify the Java String.format function.

Parameters
fa function application
Returns
A string expression representing the return value of the String.format function on the given arguments, assuming the first argument in the function application is a constant. Otherwise the first argument is returned.

Definition at line 460 of file string_constraint_generator_format.cpp.

References function_application_exprt::arguments(), char_array_of_pointer(), messaget::eom(), from_integer(), get_string_expr(), message, PRECONDITION, to_array_expr(), to_constant_expr(), to_unsigned_integer(), exprt::type(), utf16_constant_array_to_java(), and messaget::warning().

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_format() [2/2]

exprt string_constraint_generatort::add_axioms_for_format ( const array_string_exprt res,
const std::string &  s,
const exprt::operandst args 
)
private

◆ add_axioms_for_format_specifier()

array_string_exprt string_constraint_generatort::add_axioms_for_format_specifier ( const format_specifiert fs,
const struct_exprt arg,
const typet index_type,
const typet char_type 
)
private

Parse s and add axioms ensuring the output corresponds to the output of String.format.

Assumes the argument is a structured expression which contains the fields: string expr, int, float, char, boolean, hashcode, date_time. The correct component will be fetched depending on the format specifier.

Parameters
fsa format specifier
arga struct containing the possible value of the argument to format
index_typetype for indexes in strings
char_typetype of characters
Returns
String expression representing the output of String.format.

Definition at line 260 of file string_constraint_generator_format.cpp.

References add_axioms_for_constant(), add_axioms_for_string_of_float(), add_axioms_for_to_upper_case(), add_axioms_from_bool(), add_axioms_from_char(), add_axioms_from_float_scientific_notation(), add_axioms_from_int(), add_axioms_from_int_hex(), string_constraint_generatort::format_specifiert::BOOLEAN, string_constraint_generatort::format_specifiert::BOOLEAN_UPPER, char_type(), string_constraint_generatort::format_specifiert::CHARACTER, string_constraint_generatort::format_specifiert::CHARACTER_UPPER, string_constraint_generatort::format_specifiert::conversion, string_constraint_generatort::format_specifiert::DATE_TIME, string_constraint_generatort::format_specifiert::DATE_TIME_UPPER, string_constraint_generatort::format_specifiert::DECIMAL_FLOAT, string_constraint_generatort::format_specifiert::DECIMAL_INTEGER, messaget::eom(), messaget::error(), fresh_string(), string_constraint_generatort::format_specifiert::GENERAL, string_constraint_generatort::format_specifiert::GENERAL_UPPER, get_component_in_struct(), get_string_expr(), string_constraint_generatort::format_specifiert::HASHCODE, string_constraint_generatort::format_specifiert::HASHCODE_UPPER, string_constraint_generatort::format_specifiert::HEXADECIMAL_FLOAT, string_constraint_generatort::format_specifiert::HEXADECIMAL_FLOAT_UPPER, string_constraint_generatort::format_specifiert::HEXADECIMAL_INTEGER, index_type(), INVARIANT, string_constraint_generatort::format_specifiert::LINE_SEPARATOR, message, string_constraint_generatort::format_specifiert::OCTAL_INTEGER, string_constraint_generatort::format_specifiert::PERCENT_SIGN, string_constraint_generatort::format_specifiert::SCIENTIFIC, string_constraint_generatort::format_specifiert::SCIENTIFIC_UPPER, string_constraint_generatort::format_specifiert::STRING, string_constraint_generatort::format_specifiert::STRING_UPPER, and messaget::warning().

Referenced by add_axioms_for_format().

◆ add_axioms_for_fractional_part()

exprt string_constraint_generatort::add_axioms_for_fractional_part ( const array_string_exprt res,
const exprt int_expr,
size_t  max_size 
)
private

Add axioms for representing the fractional part of a floating point starting with a dot.

Parameters
resstring expression for the result
int_expran integer expression
max_sizea maximal size for the string, this includes the potential minus sign and therefore should be greater than 2
Returns
code 0 on success

Definition at line 229 of file string_constraint_generator_float.cpp.

References string_exprt< child_t >::axiom_for_length_gt(), string_exprt< child_t >::axiom_for_length_le(), char_type(), conjunction(), constant_char(), array_string_exprt::content(), from_integer(), irept::id(), index_type(), is_number(), lemmas, array_string_exprt::length(), PRECONDITION, typet::subtype(), and exprt::type().

Referenced by add_axioms_for_string_of_float(), and add_axioms_from_float_scientific_notation().

◆ add_axioms_for_function_application()

exprt string_constraint_generatort::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.

Axioms are then added to enforce that the result corresponds to the function application.

parameters: an expression containing a function application
Returns
expression corresponding to the result of the function application

Definition at line 410 of file string_constraint_generator_main.cpp.

References add_axioms_for_char_at(), add_axioms_for_char_literal(), add_axioms_for_char_set(), add_axioms_for_code_point_at(), add_axioms_for_code_point_before(), add_axioms_for_code_point_count(), add_axioms_for_compare_to(), add_axioms_for_concat(), add_axioms_for_concat_char(), add_axioms_for_concat_code_point(), add_axioms_for_constrain_characters(), add_axioms_for_contains(), add_axioms_for_copy(), add_axioms_for_delete(), add_axioms_for_delete_char_at(), add_axioms_for_empty_string(), add_axioms_for_equals(), add_axioms_for_equals_ignore_case(), add_axioms_for_format(), add_axioms_for_hash_code(), add_axioms_for_index_of(), add_axioms_for_insert(), add_axioms_for_insert_bool(), add_axioms_for_insert_char(), add_axioms_for_insert_double(), add_axioms_for_insert_float(), add_axioms_for_insert_int(), add_axioms_for_intern(), add_axioms_for_is_empty(), add_axioms_for_is_prefix(), add_axioms_for_is_suffix(), add_axioms_for_last_index_of(), add_axioms_for_length(), add_axioms_for_offset_by_code_point(), add_axioms_for_parse_int(), add_axioms_for_replace(), add_axioms_for_set_length(), add_axioms_for_string_of_float(), add_axioms_for_substring(), add_axioms_for_to_lower_case(), add_axioms_for_to_upper_case(), add_axioms_for_trim(), add_axioms_from_bool(), add_axioms_from_char(), add_axioms_from_double(), add_axioms_from_float_scientific_notation(), add_axioms_from_int(), add_axioms_from_int_hex(), add_axioms_from_literal(), add_axioms_from_long(), DATA_INVARIANT, get_function_name(), id2string(), and string_refinement_invariantt.

Referenced by string_builtin_function_with_no_evalt::add_constraints().

◆ add_axioms_for_hash_code()

exprt string_constraint_generatort::add_axioms_for_hash_code ( const function_application_exprt f)
private

Value that is identical for strings with the same content.

Add axioms stating that if two strings are equal then the values returned by this function are equal. These axioms are, for each string s on which hash was called:

  • \( hash(str)=hash(s) \lor |str| \ne |s| \lor (|str|=|s| \land \exists i<|s|.\ s[i]\ne str[i]) \)
    Parameters
    ffunction application with argument refined_string str
    Returns
    integer expression hash(str)

Definition at line 166 of file string_constraint_generator_comparison.cpp.

References function_application_exprt::arguments(), axiom_for_is_positive_index(), fresh_exist_index(), fresh_symbol, get_string_expr(), hash_code_of_string, index_type(), lemmas, PRECONDITION, and exprt::type().

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_index_of() [1/2]

exprt string_constraint_generatort::add_axioms_for_index_of ( const array_string_exprt str,
const exprt c,
const exprt from_index 
)
private

Add axioms stating that the returned value is the index within haystack (str) of the first occurrence of needle (c) starting the search at from_index, or is -1 if no such character occurs at or after position from_index.

These axioms are:

  1. \(-1 \le {\tt index} < |{\tt haystack}| \)
  2. \( \lnot contains \Leftrightarrow {\tt index} = -1 \)
  3. \( contains \Rightarrow {\tt from\_index} \le {\tt index} \land {\tt haystack}[{\tt index}] = {\tt needle} \)
  4. \( \forall i \in [{\tt from\_index}, {\tt index}).\ contains \Rightarrow {\tt haystack}[i] \ne {\tt needle} \)
  5. \( \forall m, n \in [{\tt from\_index}, |{\tt haystack}|) .\ \lnot contains \Rightarrow {\tt haystack}[m] \ne {\tt needle} \)
    Parameters
    stran array of characters expression
    ca character expression
    from_indexan integer expression
    Returns
    integer expression index

Definition at line 37 of file string_constraint_generator_indexof.cpp.

References constraints, fresh_boolean(), fresh_exist_index(), fresh_univ_index(), from_integer(), index_type(), lemmas, array_string_exprt::length(), and exprt::type().

Referenced by add_axioms_for_function_application(), and add_axioms_for_index_of().

◆ add_axioms_for_index_of() [2/2]

exprt string_constraint_generatort::add_axioms_for_index_of ( const function_application_exprt f)
private

Index of the first occurence of a target inside the string.

If the target is a character: Add axioms stating that the returned value is the index within haystack (str) of the first occurrence of needle (c) starting the search at from_index, or is -1 if no such character occurs at or after position from_index. (More...)

If the target is a refined_string: Add axioms stating that the returned value index is the index within haystack of the first occurrence of needle starting the search at from_index, or -1 if needle does not occur at or after position from_index. (More...)

Warning
slow for string targets
Parameters
ffunction application with arguments refined_string haystack, refined_string or character needle, and optional integer from_index with default value 0
Returns
integer expression

Definition at line 280 of file string_constraint_generator_indexof.cpp.

References add_axioms_for_index_of(), add_axioms_for_index_of_string(), function_application_exprt::arguments(), char_type(), from_integer(), get_string_expr(), irept::id(), index_type(), INVARIANT, is_refined_string_type(), PRECONDITION, string_refinement_invariantt, typet::subtype(), and exprt::type().

◆ add_axioms_for_index_of_string()

exprt string_constraint_generatort::add_axioms_for_index_of_string ( const array_string_exprt haystack,
const array_string_exprt needle,
const exprt from_index 
)
private

Add axioms stating that the returned value index is the index within haystack of the first occurrence of needle starting the search at from_index, or -1 if needle does not occur at or after position from_index.

If needle is an empty string then the result is from_index.

These axioms are:

  1. \( contains \Rightarrow {\tt from\_index} \le \tt{index} \le |{\tt haystack}|-|{\tt needle} | \)
  2. \( \lnot contains \Leftrightarrow {\tt index} = -1 \)
  3. \( \forall n \in [0,|{\tt needle}|).\ contains \Rightarrow {\tt haystack}[n + {\tt index}] = {\tt needle}[n] \)
  4. \( \forall n \in [{\tt from\_index}, {\tt index}).\ contains \Rightarrow (\exists m \in [0,|{\tt needle}|).\ {\tt haystack}[m+n] \ne {\tt needle}[m]]) \)
  5. \( \forall n \in [{\tt from\_index},|{\tt haystack}|-|{\tt needle}|] .\ \lnot contains \Rightarrow (\exists m \in [0,|{\tt needle}|) .\ {\tt haystack}[m+n] \ne {\tt needle}[m]) \)
  6. \( |{\tt needle}| = 0 \Rightarrow \tt{index} = from_index \)
    Parameters
    haystackan array of character expression
    needlean array of character expression
    from_indexan integer expression
    Returns
    integer expression index representing the first index of needle in haystack

Definition at line 106 of file string_constraint_generator_indexof.cpp.

References constraints, fresh_boolean(), fresh_exist_index(), fresh_univ_index(), from_integer(), index_type(), lemmas, array_string_exprt::length(), not_contains_constraints, and exprt::type().

Referenced by add_axioms_for_index_of().

◆ add_axioms_for_insert() [1/2]

exprt string_constraint_generatort::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.

We write offset' for max(0, min(res.length, offset)). These axioms are:

  1. res.length = s1.length + s2.length
  2. forall i < offset' . res[i] = s1[i]
  3. forall i < s2.length. res[i + offset'] = s2[i]
  4. forall i in [offset', s1.length). res[i + s2.length] = s1[i] This is equivalent to ‘res=concat(substring(s1, 0, offset’), concat(s2, substring(s1, offset')))`.
    Parameters
    resarray of characters expression
    s1array of characters expression
    s2array of characters expression
    offsetinteger expression
    Returns
    an expression expression which is different from zero if there is an exception to signal

Definition at line 32 of file string_constraint_generator_insert.cpp.

References constraints, fresh_symbol, from_integer(), get_return_code_type(), index_type(), lemmas, length_constraint_for_insert(), maximum(), minimum(), PRECONDITION, and exprt::type().

Referenced by add_axioms_for_function_application(), add_axioms_for_insert(), add_axioms_for_insert_char(), and string_insertion_builtin_functiont::add_constraints().

◆ add_axioms_for_insert() [2/2]

exprt string_constraint_generatort::add_axioms_for_insert ( const function_application_exprt f)
private

Insertion of a string in another at a specific index.

Add axioms ensuring the result res corresponds to s1 where we inserted s2 at position offset. (More...)

If start and end arguments are given then substring(s2, start, end) is considered instead of s2.

Parameters
ffunction application with arguments integer |res|, character pointer &res[0], refined_string s1, refined_strings2, integer offset, optional integer start and optional integer end
Returns
an integer expression which is different from zero if there is an exception to signal

Definition at line 100 of file string_constraint_generator_insert.cpp.

References add_axioms_for_insert(), add_axioms_for_substring(), function_application_exprt::arguments(), char_array_of_pointer(), char_type(), fresh_string(), from_integer(), get_string_expr(), index_type(), PRECONDITION, typet::subtype(), and exprt::type().

◆ add_axioms_for_insert_bool()

exprt string_constraint_generatort::add_axioms_for_insert_bool ( const function_application_exprt f)
private

add axioms corresponding to the StringBuilder.insert(Z) java function

Deprecated:
should convert the value to string and call insert
Parameters
ffunction application with three arguments: a string, an integer offset, and a Boolean
Returns
a new string expression

Definition at line 156 of file string_constraint_generator_insert.cpp.

References char_type(), index_type(), PRECONDITION, and typet::subtype().

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_insert_char()

exprt string_constraint_generatort::add_axioms_for_insert_char ( const function_application_exprt f)
private

Add axioms corresponding to the StringBuilder.insert(C) java function.

Parameters
ffunction application with three arguments: a string, an integer offset, and a character
Returns
an expression

Definition at line 176 of file string_constraint_generator_insert.cpp.

References add_axioms_for_insert(), add_axioms_from_char(), function_application_exprt::arguments(), char_array_of_pointer(), char_type(), fresh_string(), get_string_expr(), index_type(), PRECONDITION, and typet::subtype().

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_insert_double()

exprt string_constraint_generatort::add_axioms_for_insert_double ( const function_application_exprt f)
private

add axioms corresponding to the StringBuilder.insert(D) java function

Deprecated:
should convert the value to string and call insert
Parameters
ffunction application with three arguments: a string, an integer offset, and a double
Returns
a string expression

Definition at line 197 of file string_constraint_generator_insert.cpp.

References char_type(), index_type(), PRECONDITION, and typet::subtype().

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_insert_float()

exprt string_constraint_generatort::add_axioms_for_insert_float ( const function_application_exprt f)
private

Add axioms corresponding to the StringBuilder.insert(F) java function.

Deprecated:
should convert the value to string and call insert
Parameters
ffunction application with three arguments: a string, an integer offset, and a float
Returns
a new string expression

Definition at line 219 of file string_constraint_generator_insert.cpp.

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_insert_int()

exprt string_constraint_generatort::add_axioms_for_insert_int ( const function_application_exprt f)
private

add axioms corresponding to the StringBuilder.insert(I) java function

Deprecated:
should convert the value to string and call insert
Parameters
ffunction application with three arguments: a string, an integer offset, and an integer
Returns
an expression

Definition at line 135 of file string_constraint_generator_insert.cpp.

References char_type(), index_type(), PRECONDITION, and typet::subtype().

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_intern()

symbol_exprt string_constraint_generatort::add_axioms_for_intern ( const function_application_exprt f)
private

Add axioms corresponding to the String.intern java function.

Add axioms stating that the return value for two equal string should be the same.

Deprecated:
Not tested.
Deprecated:
never tested
Parameters
ffunction application with one string argument
Returns
a string expression

Definition at line 272 of file string_constraint_generator_comparison.cpp.

References disjunction(), index_type(), and PRECONDITION.

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_is_empty()

exprt string_constraint_generatort::add_axioms_for_is_empty ( const function_application_exprt f)
private

Add axioms stating that the returned value is true exactly when the argument string is empty.

Deprecated:
should use string_length(s)==0 instead
Parameters
ffunction application with a string argument
Returns
a Boolean expression

Definition at line 111 of file string_constraint_generator_testing.cpp.

References string_exprt< child_t >::axiom_for_has_length(), irept::id(), is_empty(), and PRECONDITION.

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_is_prefix() [1/2]

exprt string_constraint_generatort::add_axioms_for_is_prefix ( const array_string_exprt prefix,
const array_string_exprt str,
const exprt offset 
)
private

Add axioms stating that the returned expression is true exactly when the offset is greater or equal to 0 and the first string is a prefix of the second one, starting at position offset.

These axioms are:

  1. isprefix => offset_within_bounds
  2. forall qvar in [0, |prefix|). isprefix => str[qvar + offset] = prefix[qvar]
  3. !isprefix => !offset_within_bounds || 0 <= witness < |prefix| && str[witness+offset] != prefix[witness]

where offset_within_bounds is: offset >= 0 && offset <= |str| && |str| - offset >= |prefix|

Parameters
prefixan array of characters
stran array of characters
offsetan integer
Returns
Boolean expression isprefix

Definition at line 36 of file string_constraint_generator_testing.cpp.

References axiom_for_is_positive_index(), string_exprt< child_t >::axiom_for_length_ge(), string_exprt< child_t >::axiom_for_length_gt(), constraints, fresh_boolean(), fresh_exist_index(), fresh_univ_index(), from_integer(), index_type(), lemmas, array_string_exprt::length(), exprt::type(), and witness.

Referenced by add_axioms_for_function_application(), and add_axioms_for_is_prefix().

◆ add_axioms_for_is_prefix() [2/2]

exprt string_constraint_generatort::add_axioms_for_is_prefix ( const function_application_exprt f,
bool  swap_arguments = false 
)
private

Test if the target is a prefix of the string.

Add axioms ensuring the return value is true when the string starts with the given target. These axioms are detailed here: string_constraint_generatort::add_axioms_for_is_prefix(const array_string_exprt &prefix, const array_string_exprt &str, const exprt &offset)

Parameters
fa function application with arguments refined_string s0, refined string s1 and optional integer argument offset whose default value is 0
swap_argumentsa Boolean telling whether the prefix is the second argument or the first argument
Returns
boolean expression isprefix

Definition at line 92 of file string_constraint_generator_testing.cpp.

References add_axioms_for_is_prefix(), function_application_exprt::arguments(), from_integer(), get_string_expr(), irept::id(), PRECONDITION, and exprt::type().

◆ add_axioms_for_is_suffix()

exprt string_constraint_generatort::add_axioms_for_is_suffix ( const function_application_exprt f,
bool  swap_arguments = false 
)
private

Test if the target is a suffix of the string.

Add axioms ensuring the return value is true when the first string ends with the given target. These axioms are:

  1. \( \texttt{issuffix} \Rightarrow |s_0| \ge |s_1| \)
  2. \( \forall i <|s_1|.\ {\tt issuffix} \Rightarrow s_1[i] = s_0[i + |s_0| - |s_1|] \)
  3. \( \lnot {\tt issuffix} \Rightarrow (|s_1| > |s_0| \land {\tt witness}=-1) \lor (|s_1| > {witness} \ge 0 \land s_1[{witness}] \ne s_0[{witness} + |s_0| - |s_1|] \)
Parameters
fa function application with arguments refined_string s0 and refined_string s1
swap_argumentsboolean flag telling whether the suffix is the second argument or the first argument
Returns
Boolean expression issuffix

Definition at line 148 of file string_constraint_generator_testing.cpp.

References from_integer(), irept::id(), index_type(), and PRECONDITION.

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_last_index_of() [1/2]

exprt string_constraint_generatort::add_axioms_for_last_index_of ( const array_string_exprt str,
const exprt c,
const exprt from_index 
)
private

Add axioms stating that the returned value is the index within haystack (str) of the last occurrence of needle (c) starting the search backward at from_index, or -1 if no such character occurs at or before position from_index.

These axioms are :

  1. \( -1 \le {\tt index} \le {\tt from\_index} \land {\tt index} < |{\tt haystack}| \)
  2. \( {\tt index} = -1 \Leftrightarrow \lnot contains\)
  3. \( contains \Rightarrow {\tt haystack}[{\tt index}] = {\tt needle} )\)
  4. \( \forall n \in [{\tt index} +1, min({\tt from\_index}+1, |{\tt haystack}|)) .\ contains \Rightarrow {\tt haystack}[n] \ne {\tt needle} \)
  5. \( \forall m \in [0, min({\tt from\_index}+1, |{\tt haystack}|)) .\ \lnot contains \Rightarrow {\tt haystack}[m] \ne {\tt needle}\)
    Parameters
    stran array of characters expression
    ca character expression
    from_indexan integer expression
    Returns
    integer expression index representing the last index of needle in haystack before or at from_index, or -1 if there is none

Definition at line 332 of file string_constraint_generator_indexof.cpp.

References constraints, fresh_boolean(), fresh_exist_index(), fresh_univ_index(), from_integer(), index_type(), lemmas, array_string_exprt::length(), and exprt::type().

Referenced by add_axioms_for_function_application(), and add_axioms_for_last_index_of().

◆ add_axioms_for_last_index_of() [2/2]

exprt string_constraint_generatort::add_axioms_for_last_index_of ( const function_application_exprt f)
private

Index of the last occurence of a target inside the string.

If the target is a character: Add axioms stating that the returned value is the index within haystack (str) of the last occurrence of needle (c) starting the search backward at from_index, or -1 if no such character occurs at or before position from_index. (More...)

If the target is a refined_string: Add axioms stating that the returned value is the index within haystack of the last occurrence of needle starting the search backward at from_index (ie the index is smaller or equal to from_index), or -1 if needle does not occur before from_index. (More...)

Warning
slow for string targets
Parameters
ffunction application with arguments refined_string haystack, refined_string or character needle, and optional integer from_index with default value |haystack|-1
Returns
an integer expression

Definition at line 397 of file string_constraint_generator_indexof.cpp.

References add_axioms_for_last_index_of(), add_axioms_for_last_index_of_string(), function_application_exprt::arguments(), char_type(), get_string_expr(), irept::id(), index_type(), PRECONDITION, typet::subtype(), and exprt::type().

◆ add_axioms_for_last_index_of_string()

exprt string_constraint_generatort::add_axioms_for_last_index_of_string ( const array_string_exprt haystack,
const array_string_exprt needle,
const exprt from_index 
)
private

Add axioms stating that the returned value is the index within haystack of the last occurrence of needle starting the search backward at from_index (ie the index is smaller or equal to from_index), or -1 if needle does not occur before from_index.

If needle is the empty string, the result is from_index.

These axioms are:

  1. \( contains \Rightarrow -1 \le {\tt index} \land {\tt index} \le {\tt from\_index} \land {\tt index} \le |{\tt haystack}| - |{\tt needle}| \)
  2. \( \lnot contains \Leftrightarrow {\tt index}= -1 \)
  3. \( \forall n \in [0, |{\tt needle}|).\ contains \Rightarrow {\tt haystack}[n+{\tt index}] = {\tt needle}[n] \)
  4. \( \forall n \in [{\tt index}+1, min({\tt from\_index}, |{\tt haystack}| - |{\tt needle}|)] .\ contains \Rightarrow (\exists m \in [0,|{\tt needle}|) .\ {\tt haystack}[m+n] \ne {\tt needle}[m]]) \)
  5. \( \forall n \in [0, min({\tt from\_index}, |{\tt haystack}| - |{\tt needle}|)] .\ \lnot contains \Rightarrow (\exists m \in [0,|{\tt needle}|) .\ {\tt haystack}[m+n] \ne {\tt needle}[m]) \)
  6. \( |{\tt needle}| = 0 \Rightarrow index = from_index \)
    Parameters
    haystackan array of characters expression
    needlean array of characters expression
    from_indexinteger expression
    Returns
    integer expression index representing the last index of needle in haystack before or at from_index, or -1 if there is none

Definition at line 198 of file string_constraint_generator_indexof.cpp.

References constraints, fresh_boolean(), fresh_exist_index(), fresh_univ_index(), from_integer(), index_type(), lemmas, array_string_exprt::length(), not_contains_constraints, and exprt::type().

Referenced by add_axioms_for_last_index_of().

◆ add_axioms_for_length()

exprt string_constraint_generatort::add_axioms_for_length ( const function_application_exprt f)
private

Length of a string.

Returns the length of the string argument of the given function application

Parameters
ffunction application with argument string str
Returns
expression |str|

Definition at line 557 of file string_constraint_generator_main.cpp.

References function_application_exprt::arguments(), get_string_expr(), array_string_exprt::length(), and PRECONDITION.

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_offset_by_code_point()

exprt string_constraint_generatort::add_axioms_for_offset_by_code_point ( const function_application_exprt f)
private

Add axioms corresponding the String.offsetByCodePointCount java function.

add axioms giving approximate bounds on the result of the String.offsetByCodePointCount java function.

Deprecated:
This is Java specific and should be implemented in Java.

We approximate the result by saying the result is between index + offset and index + 2 * offset

Parameters
ffunction application with arguments string str, integer index and integer offset.
Returns
a new string expression

Definition at line 203 of file string_constraint_generator_code_points.cpp.

References function_application_exprt::arguments(), fresh_symbol, lemmas, maximum(), minimum(), PRECONDITION, and exprt::type().

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_parse_int()

exprt string_constraint_generatort::add_axioms_for_parse_int ( const function_application_exprt f)
private

Integer value represented by a string.

Add axioms ensuring the value of the returned integer corresponds to the value represented by str

Parameters
fa function application with arguments refined_string str and an optional integer for the radix
Returns
integer expression equal to the value represented by str
Note
the only thing stopping us from taking longer strings with many leading zeros is the axioms for correct number format

Definition at line 491 of file string_constraint_generator_valueof.cpp.

References add_axioms_for_characters_in_integer_string(), add_axioms_for_correct_number_format(), function_application_exprt::arguments(), char_type(), fresh_symbol, from_integer(), get_string_expr(), max_printed_string_length(), PRECONDITION, typet::subtype(), to_integer_or_default(), and exprt::type().

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_replace()

exprt string_constraint_generatort::add_axioms_for_replace ( const function_application_exprt f)
private

Replace a character by another in a string.

Add axioms ensuring that res corresponds to str where occurences of old_char have been replaced by new_char. These axioms are:

  1. \( |{\tt res}| = |{\tt str}| \)
  2. \( \forall i \in 0, |{\tt res}|) .\ {\tt str}[i]={\tt old\_char} \Rightarrow {\tt res}[i]={\tt new\_char} \land {\tt str}[i]\ne {\tt old\_char} \Rightarrow {\tt res}[i]={\tt str}[i] \) Only supports String.replace(char, char) and String.replace(String, String) for single-character strings Returns original string in every other case (that behaviour is to be fixed in the future)
    Parameters
    ffunction application with arguments integer |res|, character pointer &res[0], refined_string str, character old_char and character new_char
    Returns
    an integer expression equal to 0

Definition at line 467 of file string_constraint_generator_transformation.cpp.

References function_application_exprt::arguments(), char_array_of_pointer(), constraints, fresh_univ_index(), from_integer(), get_string_expr(), lemmas, PRECONDITION, to_char_pair(), and exprt::type().

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_set_length()

exprt string_constraint_generatort::add_axioms_for_set_length ( const function_application_exprt f)
private

Reduce or extend a string to have the given length.

Add axioms ensuring the returned string expression res has length k and characters at position i in res are equal to the character at position i in s1 if i is smaller that the length of s1, otherwise it is the null character \u0000.

These axioms are:

  1. \( |{\tt res}|={\tt k} \)
  2. \( \forall i<|{\tt res}|.\ i < |s_1| \Rightarrow {\tt res}[i] = s_1[i] \)
  3. \( \forall i<|{\tt res}|.\ i \ge |s_1| \Rightarrow {\tt res}[i] = 0 \)
    Parameters
    ffunction application with arguments integer |res|, character pointer &res[0], refined_string s1, integer k
    Returns
    integer expressino equal to 0

Definition at line 35 of file string_constraint_generator_transformation.cpp.

References function_application_exprt::arguments(), char_array_of_pointer(), char_type(), constant_char(), constraints, fresh_univ_index(), from_integer(), get_string_expr(), index_type(), lemmas, minimum(), PRECONDITION, and typet::subtype().

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_string_of_float() [1/2]

exprt string_constraint_generatort::add_axioms_for_string_of_float ( const function_application_exprt f)
private

String representation of a float value.

We currently only specify that the string for NaN is "NaN", for infinity and minus infinity the string are "Infinity" and "-Infinity respectively otherwise the string contains only characters in [0123456789.] and '-' at the start for negative number

Add axioms corresponding to the String.valueOf(F) java function

Parameters
ffunction application with one float argument
Returns
an integer expression

Definition at line 155 of file string_constraint_generator_float.cpp.

References function_application_exprt::arguments(), char_array_of_pointer(), and PRECONDITION.

Referenced by add_axioms_for_format_specifier(), add_axioms_for_function_application(), and add_axioms_from_double().

◆ add_axioms_for_string_of_float() [2/2]

exprt string_constraint_generatort::add_axioms_for_string_of_float ( const array_string_exprt res,
const exprt f 
)
private

Add axioms corresponding to the integer part of m, in decimal form with no leading zeroes, followed by '.

', followed by one or more decimal digits representing the fractional part of m. This specification is correct for inputs that do not exceed 100000 and the function is unspecified for other values.

Parameters
resstring expression corresponding to the result
fexpression representing a float
Returns
an integer expression, different from zero if an error should be raised

Definition at line 185 of file string_constraint_generator_float.cpp.

References add_axioms_for_concat(), add_axioms_for_fractional_part(), add_axioms_from_int(), char_type(), constant_float(), array_string_exprt::content(), floatbv_mult(), fresh_string(), from_integer(), index_type(), array_string_exprt::length(), round_expr_to_zero(), typet::subtype(), to_floatbv_type(), and exprt::type().

◆ add_axioms_for_substring() [1/2]

exprt string_constraint_generatort::add_axioms_for_substring ( const array_string_exprt res,
const array_string_exprt str,
const exprt start,
const exprt end 
)
private

Add axioms ensuring that res corresponds to the substring of str between indexes ‘start’ = max(start, 0)and end' = max(min(end, |str|), start')`.

An actual java program should throw an exception in that case.

These axioms are:

  1. \( |{\tt res}| = end' - start' \)
  2. \( \forall i<|{\tt res}|.\ {\tt res}[i]={\tt str}[{\tt start'}+i] \)
    Parameters
    resarray of characters expression
    strarray of characters expression
    startinteger expression
    endinteger expression
    Returns
    integer expression equal to zero

Definition at line 114 of file string_constraint_generator_transformation.cpp.

References constraints, fresh_univ_index(), from_integer(), index_type(), lemmas, array_string_exprt::length(), maximum(), minimum(), PRECONDITION, and exprt::type().

Referenced by add_axioms_for_delete(), add_axioms_for_format(), add_axioms_for_function_application(), add_axioms_for_insert(), and add_axioms_for_substring().

◆ add_axioms_for_substring() [2/2]

exprt string_constraint_generatort::add_axioms_for_substring ( const function_application_exprt f)
private

Substring of a string between two indices.

Add axioms ensuring that res corresponds to the substring of str between indexes ‘start’ = max(start, 0)and end' = max(min(end, |str|), start')`. (More...)

Warning
The specification may not be correct for the case where the string is shorter than the end index
Parameters
ffunction application with arguments integer |res|, character pointer &res[0], refined_string str, integer start, optional integer end with default value |str|.
Returns
integer expression which is different from 0 when there is an exception to signal

Definition at line 88 of file string_constraint_generator_transformation.cpp.

References add_axioms_for_substring(), function_application_exprt::arguments(), char_array_of_pointer(), get_string_expr(), and PRECONDITION.

◆ add_axioms_for_to_lower_case()

exprt string_constraint_generatort::add_axioms_for_to_lower_case ( const function_application_exprt f)
private

Conversion of a string to lower case.

Add axioms ensuring res corresponds to str in which uppercase characters have been converted to lowercase. These axioms are:

  1. \( |{\tt res}| = |{\tt str}| \)
  2. \( \forall i<|{\tt str}|.\ {\tt is\_upper\_case}({\tt str}[i])? {\tt res}[i]={\tt str}[i]+diff : {\tt res}[i]={\tt str}[i] \land {\tt str}[i]<{\tt 0x100} \) where diff is the difference between lower case and upper case characters: ‘diff = 'a’-'A' = 0x20`.
Parameters
ffunction application with arguments integer |res|, character pointer &res[0], refined_string str
Returns
integer expression which is different from 0 when there is an exception to signal

Definition at line 243 of file string_constraint_generator_transformation.cpp.

References function_application_exprt::arguments(), char_array_of_pointer(), char_type(), constant_char(), constraints, disjunction(), fresh_univ_index(), from_integer(), get_string_expr(), index_type(), lemmas, PRECONDITION, to_refined_string_type(), and exprt::type().

Referenced by add_axioms_for_function_application().

◆ add_axioms_for_to_upper_case() [1/2]

exprt string_constraint_generatort::add_axioms_for_to_upper_case ( const function_application_exprt f)
private

Conversion of a string to upper case.

Add axioms ensuring res corresponds to str in which lowercase characters have been converted to uppercase. (More...)

Parameters
ffunction application with arguments integer |res|, character pointer &res[0], refined_string str
Returns
integer expression which is different from 0 when there is an exception to signal

Definition at line 367 of file string_constraint_generator_transformation.cpp.

References function_application_exprt::arguments(), char_array_of_pointer(), get_string_expr(), and PRECONDITION.

Referenced by add_axioms_for_format_specifier(), and add_axioms_for_function_application().

◆ add_axioms_for_to_upper_case() [2/2]

exprt string_constraint_generatort::add_axioms_for_to_upper_case ( const array_string_exprt res,
const array_string_exprt str 
)
private

Add axioms ensuring res corresponds to str in which lowercase characters have been converted to uppercase.

These axioms are:

  1. \( |{\tt res}| = |{\tt str}| \)
  2. \( \forall i<|{\tt str}|.\ 'a'\le {\tt str}[i]\le 'z' \Rightarrow {\tt res}[i]={\tt str}[i]+'A'-'a' \)
  3. \( \forall i<|{\tt str}|.\ \lnot ('a'\le {\tt str}[i] \le 'z') \Rightarrow {\tt res}[i]={\tt str}[i] \) Note that index expressions are only allowed in the body of universal axioms, so we use a trivial premise and push our premise into the body.
Parameters
resarray of characters expression
strarray of characters expression
Returns
integer expression which is different from 0 when there is an exception to signal

Definition at line 318 of file string_constraint_generator_transformation.cpp.

References char_type(), constant_char(), constraints, array_string_exprt::content(), convert(), fresh_univ_index(), from_integer(), index_type(), lemmas, array_string_exprt::length(), typet::subtype(), and exprt::type().

◆ add_axioms_for_trim()

exprt string_constraint_generatort::add_axioms_for_trim ( const function_application_exprt f)
private

Remove leading and trailing whitespaces.

Add axioms ensuring res corresponds to str from which leading and trailing whitespaces have been removed. Are considered whitespaces, characters whose ascii code are smaller than that of ' ' (space).

These axioms are:

  1. \( idx + |{\tt res}| \le |{\tt str}| \) where idx represents the index of the first non-space character.
  2. \( idx \ge 0 \)
  3. \( |{\tt str}| \ge idx \)
  4. \( |{\tt res}| \ge 0 \)
  5. \( |{\tt res}| \le |{\tt str}| \) (this is necessary to prevent exceeding the biggest integer)
  6. \( \forall n<m.\ {\tt str}[n] \le \lq~\rq \)
  7. \( \forall n<|{\tt str}|-m-|{\tt res}|.\ {\tt str}[m+|{\tt res}|+n] \le \lq~\rq \)
  8. \( \forall n<|{\tt res}|.\ {\tt str}[idx+n]={\tt res}[n] \)
  9. \( (s[m]>{\tt \lq~\rq} \land s[m+|{\tt res}|-1]>{\tt \lq~\rq}) \lor m=|{\tt res}| \)
    Note
    Some of the constraints among 1, 2, 3, 4 and 5 seems to be redundant
    Parameters
    ffunction application with arguments integer |res|, character pointer &res[0], refined_string str.
    Returns
    integer expression which is different from 0 when there is an exception to signal

Definition at line 166 of file string_constraint_generator_transformation.cpp.

References function_application_exprt::arguments(), char_array_of_pointer(), char_type(), constraints, fresh_exist_index(), fresh_univ_index(), from_integer(), get_string_expr(), index_type(), lemmas, PRECONDITION, typet::subtype(), and exprt::type().

Referenced by add_axioms_for_function_application().

◆ add_axioms_from_bool() [1/2]

exprt string_constraint_generatort::add_axioms_from_bool ( const function_application_exprt f)
private

Add axioms corresponding to the String.valueOf(Z) java function.

Deprecated:
This is Java specific and should be implemented in Java instead
Parameters
ffunction application with a Boolean argument
Returns
a new string expression

Definition at line 63 of file string_constraint_generator_valueof.cpp.

References PRECONDITION.

Referenced by add_axioms_for_format_specifier(), and add_axioms_for_function_application().

◆ add_axioms_from_bool() [2/2]

exprt string_constraint_generatort::add_axioms_from_bool ( const array_string_exprt res,
const exprt b 
)
private

Add axioms stating that the returned string equals "true" when the Boolean expression is true and "false" when it is false.

Deprecated:
This is Java specific and should be implemented in Java instead
Parameters
resstring expression for the result
bBoolean expression
Returns
code 0 on success

Definition at line 79 of file string_constraint_generator_valueof.cpp.

References char_type(), from_integer(), irept::id(), PRECONDITION, and typet::subtype().

◆ add_axioms_from_char() [1/2]

exprt string_constraint_generatort::add_axioms_from_char ( const function_application_exprt f)
private

Conversion from char to string.

Add axiom stating that string res has length 1 and the character it contains equals c. (More...)

Parameters
ffunction application with arguments integer |res|, character pointer &res[0] and character c
Returns
code 0 on success

Definition at line 282 of file string_constraint_generator_valueof.cpp.

References function_application_exprt::arguments(), char_array_of_pointer(), and PRECONDITION.

Referenced by add_axioms_for_format_specifier(), add_axioms_for_function_application(), and add_axioms_for_insert_char().

◆ add_axioms_from_char() [2/2]

exprt string_constraint_generatort::add_axioms_from_char ( const array_string_exprt res,
const exprt c 
)
private

Add axiom stating that string res has length 1 and the character it contains equals c.

This axiom is: \( |{\tt res}| = 1 \land {\tt res}[0] = {\tt c} \).

Parameters
resarray of characters expression
ccharacter expression
Returns
code 0 on success

Definition at line 298 of file string_constraint_generator_valueof.cpp.

References string_exprt< child_t >::axiom_for_has_length(), from_integer(), get_return_code_type(), and lemmas.

◆ add_axioms_from_double()

exprt string_constraint_generatort::add_axioms_from_double ( const function_application_exprt f)
private

Add axioms corresponding to the String.valueOf(D) java function.

Parameters
ffunction application with one double argument
Returns
an integer expression

Definition at line 167 of file string_constraint_generator_float.cpp.

References add_axioms_for_string_of_float().

Referenced by add_axioms_for_function_application().

◆ add_axioms_from_float_scientific_notation() [1/2]

exprt string_constraint_generatort::add_axioms_from_float_scientific_notation ( const array_string_exprt res,
const exprt f 
)
private

Add axioms to write the float in scientific notation.

A float is represented as \(f = m * 2^e\) where \(0 <= m < 2\) is the significand and \(-126 <= e <= 127\) is the exponent. We want an alternate representation by finding \(n\) and \(d\) such that \(f=n*10^d\). We can estimate \(d\) the following way: \(d ~= log_10(f/n) ~= log_10(m) + log_10(2) * e - log_10(n)\) \(d = floor(log_10(2) * e)\) Then \(n\) can be expressed by the equation: \(log_10(n) = log_10(m) + log_10(2) * e - d\) \(n = f / 10^d = m * 2^e / 10^d = m * 2^e / 10^(floor(log_10(2) * e))\)

Parameters
resstring expression representing the float in scientific notation
fa float expression, which is positive
Returns
a integer expression different from 0 to signal an exception

Definition at line 315 of file string_constraint_generator_float.cpp.

References add_axioms_for_concat(), add_axioms_for_constant(), add_axioms_for_fractional_part(), add_axioms_from_int(), char_type(), constant_float(), array_string_exprt::content(), estimate_decimal_exponent(), float_type(), floatbv_mult(), floatbv_of_int_expr(), fresh_string(), from_integer(), get_exponent(), get_significand(), index_type(), array_string_exprt::length(), round_expr_to_zero(), ieee_floatt::ROUND_TO_ZERO, ieee_float_spect::single_precision(), typet::subtype(), ieee_float_spect::to_type(), and exprt::type().

Referenced by add_axioms_for_format_specifier(), add_axioms_for_function_application(), and add_axioms_from_float_scientific_notation().

◆ add_axioms_from_float_scientific_notation() [2/2]

exprt string_constraint_generatort::add_axioms_from_float_scientific_notation ( const function_application_exprt f)
private

Representation of a float value in scientific notation.

Add axioms corresponding to the scientific representation of floating point values

Parameters
fa function application expression
Returns
code 0 on success

Definition at line 482 of file string_constraint_generator_float.cpp.

References add_axioms_from_float_scientific_notation(), function_application_exprt::arguments(), char_array_of_pointer(), and PRECONDITION.

◆ add_axioms_from_int() [1/2]

exprt string_constraint_generatort::add_axioms_from_int ( const function_application_exprt f)
private

Convert an integer to a string.

Add axioms corresponding to the String.valueOf(I) java function.

Parameters
ffunction application with one integer argument
Returns
a new string expression

Definition at line 27 of file string_constraint_generator_valueof.cpp.

References add_axioms_from_int_with_radix(), function_application_exprt::arguments(), char_array_of_pointer(), and PRECONDITION.

Referenced by add_axioms_for_format_specifier(), add_axioms_for_function_application(), add_axioms_for_string_of_float(), and add_axioms_from_float_scientific_notation().

◆ add_axioms_from_int() [2/2]

exprt string_constraint_generatort::add_axioms_from_int ( const array_string_exprt res,
const exprt input_int,
size_t  max_size = 0 
)
private

Add axioms enforcing that the string corresponds to the result of String.valueOf(I) or String.valueOf(J) Java functions applied on the integer expression.

Parameters
resstring expression for the result
input_inta signed integer expression
max_sizea maximal size for the string representation (default 0, which is interpreted to mean "as large as is needed for this type")
Returns
code 0 on success

Definition at line 127 of file string_constraint_generator_valueof.cpp.

References add_axioms_from_int_with_radix(), from_integer(), and exprt::type().

◆ add_axioms_from_int_hex() [1/2]

exprt string_constraint_generatort::add_axioms_from_int_hex ( const array_string_exprt res,
const exprt i 
)
private

Add axioms stating that the string res corresponds to the integer argument written in hexadecimal.

Deprecated:
use add_axioms_from_int which takes a radix argument instead
Parameters
resstring expression for the result
ian integer argument
Returns
code 0 on success

Definition at line 208 of file string_constraint_generator_valueof.cpp.

References char_type(), from_integer(), irept::id(), index_type(), is_number(), PRECONDITION, and typet::subtype().

Referenced by add_axioms_for_format_specifier(), add_axioms_for_function_application(), and add_axioms_from_int_hex().

◆ add_axioms_from_int_hex() [2/2]

exprt string_constraint_generatort::add_axioms_from_int_hex ( const function_application_exprt f)
private

Add axioms corresponding to the Integer.toHexString(I) java function.

Parameters
ffunction application with an integer argument
Returns
code 0 on success

Definition at line 263 of file string_constraint_generator_valueof.cpp.

References add_axioms_from_int_hex(), function_application_exprt::arguments(), char_array_of_pointer(), and PRECONDITION.

◆ add_axioms_from_int_with_radix()

exprt string_constraint_generatort::add_axioms_from_int_with_radix ( const array_string_exprt res,
const exprt input_int,
const exprt radix,
size_t  max_size = 0 
)
private

Add axioms enforcing that the string corresponds to the result of String.valueOf(II) or String.valueOf(JI) Java functions applied on the integer expression.

Parameters
resstring expression for the result
input_inta signed integer expression
radixthe radix to use
max_sizea maximal size for the string representation (default 0, which is interpreted to mean "as large as is needed for this type")
Returns
code 0 on success

Most of the time we can evaluate radix as an integer. The value 0 is used to indicate when we can't tell what the radix is.

Definition at line 145 of file string_constraint_generator_valueof.cpp.

References add_axioms_for_characters_in_integer_string(), add_axioms_for_correct_number_format(), char_type(), CHECK_RETURN, array_string_exprt::content(), from_integer(), irept::id(), max_printed_string_length(), PRECONDITION, typet::subtype(), to_integer_or_default(), and exprt::type().

Referenced by add_axioms_from_int().

◆ add_axioms_from_literal()

exprt string_constraint_generatort::add_axioms_from_literal ( const function_application_exprt f)
private

String corresponding to an internal cprover string.

Add axioms ensuring that the returned string expression is equal to the string literal.

Parameters
ffunction application with an argument which is a string literal that is a constant with a string value.
Returns
string expression

Definition at line 111 of file string_constraint_generator_constants.cpp.

References add_axioms_for_cprover_string(), function_application_exprt::arguments(), char_array_of_pointer(), and PRECONDITION.

Referenced by add_axioms_for_function_application().

◆ add_axioms_from_long()

exprt string_constraint_generatort::add_axioms_from_long ( const function_application_exprt f)
private

Add axioms corresponding to the String.valueOf(J) java function.

Deprecated:
should use add_axioms_from_int instead
Parameters
ffunction application with one long argument
Returns
a new string expression

Definition at line 45 of file string_constraint_generator_valueof.cpp.

References PRECONDITION.

Referenced by add_axioms_for_function_application().

◆ add_constraint_on_characters()

void string_constraint_generatort::add_constraint_on_characters ( const array_string_exprt s,
const exprt start,
const exprt end,
const std::string &  char_set 
)
private

Add constraint on characters of a string.

This constraint is \( \forall i \in [start, end), low\_char \le s[i] \le high\_char \)

Parameters
sa string expression
startindex of the first character to constrain
endindex at which we stop adding constraints
char_seta string of the form "<low_char>-<high_char>" where <low_char> and <high_char> are two characters, which represents the set of characters that are between low_char and high_char.
Returns
a string expression that is linked to the argument through axioms that are added to the list

Definition at line 309 of file string_constraint_generator_main.cpp.

References constraints, fresh_univ_index(), from_integer(), array_string_exprt::length(), PRECONDITION, and exprt::type().

Referenced by add_axioms_for_constrain_characters().

◆ add_lemma()

void string_constraint_generatort::add_lemma ( const exprt expr)

Definition at line 41 of file string_constraint_generator_main.cpp.

References lemmas.

Referenced by string_dependenciest::add_constraints().

◆ associate_array_to_pointer()

exprt string_constraint_generatort::associate_array_to_pointer ( const function_application_exprt f)
private

Associate a char array to a char pointer.

Insert in array_pool a binding from ptr to arr. If the length of arr is infinite, a new integer symbol is created and stored in array_pool. This also adds the default axioms for arr.

Parameters
fa function application with argument a character array arr and a character pointer ptr.

Definition at line 244 of file string_constraint_generator_main.cpp.

References function_application_exprt::arguments(), array_pool, created_strings, from_integer(), array_poolt::insert(), PRECONDITION, to_array_string_expr(), to_index_expr(), and exprt::type().

Referenced by make_array_pointer_association().

◆ associate_length_to_array()

exprt string_constraint_generatort::associate_length_to_array ( const function_application_exprt f)
private

Associate an integer length to a char array.

This adds an axiom ensuring that arr.length and length are equal.

Parameters
fa function application with argument a character array arr and a integer length.
Returns
integer expression equal to 0

Definition at line 266 of file string_constraint_generator_main.cpp.

References function_application_exprt::arguments(), array_pool, from_integer(), array_poolt::get_length(), lemmas, PRECONDITION, to_array_string_expr(), and exprt::type().

Referenced by make_array_pointer_association().

◆ axiom_for_is_positive_index()

exprt string_constraint_generatort::axiom_for_is_positive_index ( const exprt x)
private

expression true exactly when the index is positive

Parameters
xan index expression
Returns
a Boolean expression

Definition at line 568 of file string_constraint_generator_main.cpp.

References from_integer(), and exprt::type().

Referenced by add_axioms_for_contains(), add_axioms_for_hash_code(), and add_axioms_for_is_prefix().

◆ char_array_of_pointer()

◆ character_equals_ignore_case()

exprt string_constraint_generatort::character_equals_ignore_case ( exprt  char1,
exprt  char2,
exprt  char_a,
exprt  char_A,
exprt  char_Z 
)
staticprivate

Returns an expression which is true when the two given characters are equal when ignoring case for ASCII.

Parameters
char1character expression
char2character expression
char_aconstant character 'a'
char_Aconstant character 'A'
char_Zconstant character 'Z'
Returns
a expression of Boolean type

Definition at line 75 of file string_constraint_generator_comparison.cpp.

Referenced by add_axioms_for_equals_ignore_case().

◆ clear_constraints()

void string_constraint_generatort::clear_constraints ( )

Clear all constraints and lemmas.

Definition at line 290 of file string_constraint_generator_main.cpp.

References constraints, lemmas, and not_contains_constraints.

Referenced by string_refinementt::dec_solve().

◆ constant_char()

constant_exprt string_constraint_generatort::constant_char ( int  i,
const typet char_type 
)
staticprivate

generate constant character expression with character type.

parameters: integer representing a character, and a type for
characters; we do not use char type here because in some languages (for instance java) characters use more than 8 bits.
Returns
constant expression corresponding to the character.

Definition at line 82 of file string_constraint_generator_main.cpp.

References char_type(), and from_integer().

Referenced by add_axioms_for_characters_in_integer_string(), add_axioms_for_correct_number_format(), add_axioms_for_equals_ignore_case(), add_axioms_for_fractional_part(), add_axioms_for_set_length(), add_axioms_for_to_lower_case(), add_axioms_for_to_upper_case(), int_of_hex_char(), is_high_surrogate(), and is_low_surrogate().

◆ fresh_boolean()

symbol_exprt string_constraint_generatort::fresh_boolean ( const irep_idt prefix)
private

generate a Boolean symbol which is existentially quantified

parameters: a prefix
Returns
a symbol of index type whose name starts with the prefix

Definition at line 124 of file string_constraint_generator_main.cpp.

References boolean_symbols, and fresh_symbol.

Referenced by add_axioms_for_contains(), add_axioms_for_equals(), add_axioms_for_equals_ignore_case(), add_axioms_for_index_of(), add_axioms_for_index_of_string(), add_axioms_for_is_prefix(), add_axioms_for_last_index_of(), and add_axioms_for_last_index_of_string().

◆ fresh_exist_index()

symbol_exprt string_constraint_generatort::fresh_exist_index ( const irep_idt prefix,
const typet type 
)

◆ fresh_string()

array_string_exprt string_constraint_generatort::fresh_string ( const typet index_type,
const typet char_type 
)
private

◆ fresh_univ_index()

◆ get_boolean_symbols()

const std::vector< symbol_exprt > & string_constraint_generatort::get_boolean_symbols ( ) const

Boolean symbols for the results of some string functions.

Definition at line 65 of file string_constraint_generator_main.cpp.

References boolean_symbols.

Referenced by check_axioms().

◆ get_constraints()

const std::vector< string_constraintt > & string_constraint_generatort::get_constraints ( ) const

Definition at line 47 of file string_constraint_generator_main.cpp.

References constraints.

Referenced by string_refinementt::dec_solve().

◆ get_created_strings()

const std::set< array_string_exprt > & string_constraint_generatort::get_created_strings ( ) const

Set of strings that have been created by the generator.

Definition at line 71 of file string_constraint_generator_main.cpp.

References created_strings.

Referenced by string_refinementt::get().

◆ get_index_symbols()

const std::vector< symbol_exprt > & string_constraint_generatort::get_index_symbols ( ) const

Symbols used in existential quantifications.

Definition at line 59 of file string_constraint_generator_main.cpp.

References index_symbols.

Referenced by check_axioms().

◆ get_lemmas()

const std::vector< exprt > & string_constraint_generatort::get_lemmas ( ) const

Axioms are of three kinds: universally quantified string constraint, not contains string constraints and simple formulas.

Definition at line 36 of file string_constraint_generator_main.cpp.

References lemmas.

Referenced by string_refinementt::dec_solve().

◆ get_not_contains_constraints()

const std::vector< string_not_contains_constraintt > & string_constraint_generatort::get_not_contains_constraints ( ) const

◆ get_return_code_type()

◆ get_string_expr()

◆ get_witness_of()

exprt string_constraint_generatort::get_witness_of ( const string_not_contains_constraintt c,
const exprt univ_val 
) const
inline

Definition at line 119 of file string_constraint_generator.h.

References witness.

Referenced by check_axioms(), and string_refinementt::instantiate_not_contains().

◆ int_of_hex_char()

exprt string_constraint_generatort::int_of_hex_char ( const exprt chr)
staticprivate

Returns the integer value represented by the character.

Parameters
chra character expression in the following set: 0123456789abcdef
Returns
an integer expression

Definition at line 190 of file string_constraint_generator_valueof.cpp.

References constant_char(), and exprt::type().

◆ is_high_surrogate()

exprt string_constraint_generatort::is_high_surrogate ( const exprt chr)
staticprivate

the output is true when the character is a high surrogate for UTF-16 encoding, see https://en.wikipedia.org/wiki/UTF-16 for more explenation about the encoding; this is true when the character is in the range 0xD800..0xDBFF

Parameters
chra character expression
Returns
a Boolean expression

Definition at line 75 of file string_constraint_generator_code_points.cpp.

References constant_char(), and exprt::type().

Referenced by add_axioms_for_code_point_at(), and add_axioms_for_code_point_before().

◆ is_low_surrogate()

exprt string_constraint_generatort::is_low_surrogate ( const exprt chr)
staticprivate

the output is true when the character is a low surrogate for UTF-16 encoding, see https://en.wikipedia.org/wiki/UTF-16 for more explenation about the encoding; this is true when the character is in the range 0xDC00..0xDFFF

Parameters
chra character expression
Returns
a Boolean expression

Definition at line 88 of file string_constraint_generator_code_points.cpp.

References constant_char(), and exprt::type().

Referenced by add_axioms_for_code_point_at(), and add_axioms_for_code_point_before().

◆ make_array_pointer_association()

optionalt< exprt > string_constraint_generatort::make_array_pointer_association ( const function_application_exprt expr)

Associate array to pointer, and array to length.

Returns
an expression if the given function application is one of associate pointer and associate length

Definition at line 394 of file string_constraint_generator_main.cpp.

References associate_array_to_pointer(), associate_length_to_array(), and get_function_name().

Referenced by make_char_array_pointer_associations().

◆ to_integer_or_default()

unsigned long string_constraint_generatort::to_integer_or_default ( const exprt expr,
unsigned long  def 
)
private

If the expression is a constant expression then we get the value of it as an unsigned long.

If not we return a default value.

Parameters
exprinput expression
defdefault value to return if we cannot evaluate expr
Returns
the output as an unsigned long

Definition at line 542 of file string_constraint_generator_valueof.cpp.

References integer2ulong(), ns, simplify_expr(), and to_integer().

Referenced by add_axioms_for_parse_int(), and add_axioms_from_int_with_radix().

Member Data Documentation

◆ array_pool

◆ boolean_symbols

std::vector<symbol_exprt> string_constraint_generatort::boolean_symbols
private

Definition at line 406 of file string_constraint_generator.h.

Referenced by fresh_boolean(), and get_boolean_symbols().

◆ constraints

◆ created_strings

std::set<array_string_exprt> string_constraint_generatort::created_strings
private

◆ fresh_symbol

◆ hash_code_of_string

std::map<array_string_exprt, exprt> string_constraint_generatort::hash_code_of_string
private

Definition at line 411 of file string_constraint_generator.h.

Referenced by add_axioms_for_hash_code().

◆ index_symbols

std::vector<symbol_exprt> string_constraint_generatort::index_symbols
private

Definition at line 407 of file string_constraint_generator.h.

Referenced by fresh_exist_index(), and get_index_symbols().

◆ intern_of_string

std::map<array_string_exprt, symbol_exprt> string_constraint_generatort::intern_of_string
private

Definition at line 414 of file string_constraint_generator.h.

◆ lemmas

◆ message

const messaget string_constraint_generatort::message
private

◆ not_contains_constraints

◆ ns

const namespacet string_constraint_generatort::ns
private

Definition at line 408 of file string_constraint_generator.h.

Referenced by to_integer_or_default().

◆ witness


The documentation for this class was generated from the following files: