cprover
string_constraint_generator.h File Reference
#include <limits>
#include <util/string_expr.h>
#include <util/replace_expr.h>
#include <util/refined_string_type.h>
#include <util/constexpr.def>
#include <util/deprecate.h>
#include <solvers/refinement/string_constraint.h>
+ Include dependency graph for string_constraint_generator.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  symbol_generatort
 Generation of fresh symbols of a given type. More...
 
class  array_poolt
 Correspondance between arrays and pointers string representations. More...
 
struct  string_constraintst
 Collection of constraints of different types: existential formulas, universal formulas, and "not contains" (universal with one alternation). More...
 
class  string_constraint_generatort
 

Functions

array_string_exprt of_argument (array_poolt &array_pool, const exprt &arg)
 Converts a struct containing a length and pointer to an array. More...
 
const array_string_exprtchar_array_of_pointer (array_poolt &pool, const exprt &pointer, const exprt &length)
 Adds creates a new array if it does not already exists. More...
 
array_string_exprt get_string_expr (array_poolt &pool, const exprt &expr)
 casts an expression to a string expression, or fetches the actual string_exprt in the case of a symbol. More...
 
void merge (string_constraintst &result, string_constraintst other)
 Merge two sets of constraints by appending to the first one. More...
 
signedbv_typet get_return_code_type ()
 
std::pair< exprt, string_constraintstadd_axioms_for_concat (symbol_generatort &fresh_symbol, 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...
 
std::pair< exprt, string_constraintstadd_axioms_for_concat_substr (symbol_generatort &fresh_symbol, 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...
 
std::pair< exprt, string_constraintstadd_axioms_for_insert (symbol_generatort &fresh_symbol, 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...
 
std::pair< exprt, string_constraintstadd_axioms_for_string_of_int_with_radix (const array_string_exprt &res, const exprt &input_int, const exprt &radix, size_t max_size, const namespacet &ns)
 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...
 
string_constraintst add_constraint_on_characters (symbol_generatort &fresh_symbol, const array_string_exprt &s, const exprt &start, const exprt &end, const std::string &char_set)
 Add constraint on characters of a string. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_constrain_characters (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 Add axioms to ensure all characters of a string belong to a given set. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_char_at (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 Character at a given position. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_code_point_at (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool)
 add axioms corresponding to the String.codePointAt java function More...
 
std::pair< exprt, string_constraintstadd_axioms_for_code_point_before (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool)
 add axioms corresponding to the String.codePointBefore java function More...
 
std::pair< exprt, string_constraintstadd_axioms_for_contains (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 Test whether a string contains another. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_equals (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool)
 Equality of the content of two strings. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_equals_ignore_case (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool)
 Equality of the content ignoring case of characters. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_is_empty (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 Add axioms stating that the returned value is true exactly when the argument string is empty. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_is_prefix (symbol_generatort &fresh_symbol, 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...
 
std::pair< exprt, string_constraintstadd_axioms_for_is_prefix (symbol_generatort &fresh_symbol, const function_application_exprt &f, bool swap_arguments, array_poolt &array_pool)
 Test if the target is a prefix of the string. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_is_suffix (symbol_generatort &fresh_symbol, const function_application_exprt &f, bool swap_arguments, array_poolt &array_pool)
 Test if the target is a suffix of the string. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_length (const function_application_exprt &f, array_poolt &array_pool)
 Length of a string. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_empty_string (const function_application_exprt &f)
 Add axioms to say that the returned string expression is empty. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_copy (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 add axioms to say that the returned string expression is equal to the argument of the function application More...
 
std::pair< exprt, string_constraintstadd_axioms_for_concat_code_point (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 Add axioms corresponding to the StringBuilder.appendCodePoint(I) function. More...
 
std::pair< exprt, string_constraintstadd_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...
 
std::pair< exprt, string_constraintstadd_axioms_for_delete (symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end, array_poolt &array_pool)
 Add axioms stating that res corresponds to the input str where we removed characters between the positions start (included) and end (not included). More...
 
std::pair< exprt, string_constraintstadd_axioms_for_delete (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 Remove a portion of a string. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_delete_char_at (symbol_generatort &fresh_symbol, const function_application_exprt &expr, array_poolt &array_pool)
 add axioms corresponding to the StringBuilder.deleteCharAt java function More...
 
std::pair< exprt, string_constraintstadd_axioms_for_format (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const messaget &message, const namespacet &ns)
 Formatted string using a format string and list of arguments. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_format (symbol_generatort &fresh_symbol, const array_string_exprt &res, const std::string &s, const exprt::operandst &args, array_poolt &array_pool, const messaget &message, const namespacet &ns)
 Parse s and add axioms ensuring the output corresponds to the output of String.format. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_insert (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool)
 Insertion of a string in another at a specific index. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_insert_int (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
 add axioms corresponding to the StringBuilder.insert(I) java function More...
 
std::pair< exprt, string_constraintstadd_axioms_for_insert_bool (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 add axioms corresponding to the StringBuilder.insert(Z) java function More...
 
std::pair< exprt, string_constraintstadd_axioms_for_insert_char (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 Add axioms corresponding to the StringBuilder.insert(C) java function. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_insert_float (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
 Add axioms corresponding to the StringBuilder.insert(F) java function. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_insert_double (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
 add axioms corresponding to the StringBuilder.insert(D) java function More...
 
std::pair< exprt, string_constraintstadd_axioms_for_cprover_string (symbol_generatort &fresh_symbol, const array_string_exprt &res, const exprt &arg, const exprt &guard)
 Convert an expression of type string_typet to a string_exprt. More...
 
std::pair< exprt, string_constraintstadd_axioms_from_literal (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 String corresponding to an internal cprover string. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_string_of_int (const array_string_exprt &res, const exprt &input_int, size_t max_size, const namespacet &ns)
 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...
 
std::pair< exprt, string_constraintstadd_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...
 
std::pair< exprt, string_constraintstadd_axioms_from_int_hex (const function_application_exprt &f, array_poolt &array_pool)
 Add axioms corresponding to the Integer.toHexString(I) java function. More...
 
std::pair< exprt, string_constraintstadd_axioms_from_long (const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
 Add axioms corresponding to the String.valueOf(J) java function. More...
 
std::pair< exprt, string_constraintstadd_axioms_from_bool (const function_application_exprt &f, array_poolt &array_pool)
 Add axioms corresponding to the String.valueOf(Z) java function. More...
 
std::pair< exprt, string_constraintstadd_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...
 
std::pair< exprt, string_constraintstadd_axioms_from_char (const function_application_exprt &f, array_poolt &array_pool)
 Conversion from char to string. More...
 
std::pair< exprt, string_constraintstadd_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...
 
std::pair< exprt, string_constraintstadd_axioms_for_index_of (symbol_generatort &fresh_symbol, 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...
 
std::pair< exprt, string_constraintstadd_axioms_for_index_of_string (symbol_generatort &fresh_symbol, 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...
 
std::pair< exprt, string_constraintstadd_axioms_for_index_of (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 Index of the first occurence of a target inside the string. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_last_index_of_string (symbol_generatort &fresh_symbol, 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...
 
std::pair< exprt, string_constraintstadd_axioms_for_last_index_of (symbol_generatort &fresh_symbol, 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...
 
std::pair< exprt, string_constraintstadd_axioms_for_last_index_of (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 Index of the last occurence of a target inside the string. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_string_of_float (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
 String representation of a float value. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_string_of_float (symbol_generatort &fresh_symbol, const array_string_exprt &res, const exprt &f, array_poolt &array_pool, const namespacet &ns)
 Add axioms corresponding to the integer part of m, in decimal form with no leading zeroes, followed by '. More...
 
std::pair< exprt, string_constraintstadd_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...
 
std::pair< exprt, string_constraintstadd_axioms_from_float_scientific_notation (symbol_generatort &fresh_symbol, const array_string_exprt &res, const exprt &f, array_poolt &array_pool, const namespacet &ns)
 Add axioms to write the float in scientific notation. More...
 
std::pair< exprt, string_constraintstadd_axioms_from_float_scientific_notation (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
 Representation of a float value in scientific notation. More...
 
std::pair< exprt, string_constraintstadd_axioms_from_double (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
 Add axioms corresponding to the String.valueOf(D) java function. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_replace (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 Replace a character by another in a string. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_set_length (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 Reduce or extend a string to have the given length. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_substring (symbol_generatort &fresh_symbol, 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...
 
std::pair< exprt, string_constraintstadd_axioms_for_substring (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 Substring of a string between two indices. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_trim (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 Remove leading and trailing whitespaces. More...
 
std::pair< exprt, string_constraintstadd_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...
 
std::pair< exprt, string_constraintstadd_axioms_for_char_literal (const function_application_exprt &f)
 add axioms stating that the returned value is equal to the argument More...
 
std::pair< exprt, string_constraintstadd_axioms_for_code_point_count (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool)
 Add axioms corresponding the String.codePointCount java function. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_offset_by_code_point (symbol_generatort &fresh_symbol, const function_application_exprt &f)
 Add axioms corresponding the String.offsetByCodePointCount java function. More...
 
string_constraintst 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...
 
string_constraintst add_axioms_for_correct_number_format (const array_string_exprt &str, const exprt &radix_as_char, const unsigned long radix_ul, const std::size_t max_size, const bool strict_formatting)
 Add axioms making the return value true if the given string is a correct number in the given radix. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_parse_int (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
 Integer value represented by a string. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_compare_to (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 Lexicographic comparison of two strings. More...
 
exprt is_digit_with_radix (const exprt &chr, const bool strict_formatting, const exprt &radix_as_char, const unsigned long radix_ul)
 Check if a character is a digit with respect to the given radix, e.g. More...
 
exprt get_numeric_value_from_character (const exprt &chr, const typet &char_type, const typet &type, const bool strict_formatting, unsigned long radix_ul)
 Get the numeric value of a character, assuming that the radix is large enough. More...
 
size_t max_printed_string_length (const typet &type, unsigned long ul_radix)
 Calculate the string length needed to represent any value of the given type using the given radix. More...
 
std::string utf16_constant_array_to_java (const array_exprt &arr, std::size_t length)
 Construct a string from a constant array. More...
 
exprt is_positive (const exprt &x)
 
exprt minimum (const exprt &a, const exprt &b)
 
exprt maximum (const exprt &a, const exprt &b)
 
exprt sum_overflows (const plus_exprt &sum)
 
exprt length_constraint_for_concat_char (const array_string_exprt &res, const array_string_exprt &s1)
 Add axioms enforcing that the length of res is that of the concatenation of s1 with. More...
 
exprt length_constraint_for_concat (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
 Add axioms enforcing that the length of res is that of the concatenation of s1 with s2 More...
 
exprt length_constraint_for_concat_substr (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &start_index, const exprt &end_index)
 Add axioms enforcing that the length of res is that of the concatenation of s1 with the substring of s2 starting at index ‘start’ and ending at indexend'‘. More...
 
exprt length_constraint_for_insert (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
 Add axioms ensuring the length of res corresponds to that of s1 where we inserted s2. More...
 
exprt zero_if_negative (const exprt &expr)
 Returns a non-negative version of the argument. More...
 
std::pair< exprt, string_constraintstcombine_results (std::pair< exprt, string_constraintst > result1, std::pair< exprt, string_constraintst > result2)
 Combine the results of two add_axioms function by taking the maximum of the return codes and merging the constraints. More...
 

Detailed Description

Generates string constraints to link results from string functions with their arguments. This is inspired by the PASS paper at HVC'13: "PASS: String Solving with Parameterized Array and Interval Automaton" by Guodong Li and Indradeep Ghosh, which gives examples of constraints for several functions.

Definition in file string_constraint_generator.h.

Function Documentation

◆ add_axioms_for_char_at()

std::pair<exprt, string_constraintst> add_axioms_for_char_at ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

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
fresh_symbolgenerator of fresh symbols
ffunction application with arguments string str and integer i
array_poolpool of arrays representing strings
Returns
character expression char

Definition at line 566 of file string_constraint_generator_main.cpp.

◆ add_axioms_for_char_literal()

std::pair<exprt, string_constraintst> add_axioms_for_char_literal ( const function_application_exprt f)

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

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

Definition at line 532 of file string_constraint_generator_main.cpp.

◆ add_axioms_for_characters_in_integer_string()

string_constraintst 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.

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 415 of file string_constraint_generator_valueof.cpp.

◆ add_axioms_for_code_point()

std::pair<exprt, string_constraintst> 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

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.

◆ add_axioms_for_code_point_at()

std::pair<exprt, string_constraintst> add_axioms_for_code_point_at ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

add axioms corresponding to the String.codePointAt java function

Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with arguments a string and an index
array_poolpool of arrays representing strings
Returns
a integer expression corresponding to a code point

Definition at line 122 of file string_constraint_generator_code_points.cpp.

◆ add_axioms_for_code_point_before()

std::pair<exprt, string_constraintst> add_axioms_for_code_point_before ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

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 155 of file string_constraint_generator_code_points.cpp.

◆ add_axioms_for_code_point_count()

std::pair<exprt, string_constraintst> add_axioms_for_code_point_count ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

Add axioms corresponding the String.codePointCount java function.

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

Add axioms corresponding the String.codePointCount java function.

Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with three arguments string str, integer begin and integer end.
array_poolpool of arrays representing strings
Returns
an integer expression

Definition at line 193 of file string_constraint_generator_code_points.cpp.

◆ add_axioms_for_compare_to()

std::pair<exprt, string_constraintst> add_axioms_for_compare_to ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt pool 
)

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
    fresh_symbolgenerator of fresh symbols
    ffunction application with arguments refined_string s1 and refined_string s2
    poolpool of arrays representing strings
    Returns
    integer expression res

Definition at line 241 of file string_constraint_generator_comparison.cpp.

◆ add_axioms_for_concat()

std::pair<exprt, string_constraintst> add_axioms_for_concat ( symbol_generatort fresh_symbol,
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
fresh_symbolgenerator of fresh symbols
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 126 of file string_constraint_generator_concat.cpp.

◆ add_axioms_for_concat_code_point()

std::pair<exprt, string_constraintst> add_axioms_for_concat_code_point ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

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

Deprecated:
java specific
Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with two arguments: a string and a code point
array_poolpool of arrays representing strings
Returns
an expression

Definition at line 143 of file string_constraint_generator_concat.cpp.

◆ add_axioms_for_concat_substr()

std::pair<exprt, string_constraintst> add_axioms_for_concat_substr ( symbol_generatort fresh_symbol,
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
fresh_symbolgenerator of fresh symbols
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 38 of file string_constraint_generator_concat.cpp.

◆ add_axioms_for_constant()

std::pair<exprt, string_constraintst> add_axioms_for_constant ( const array_string_exprt res,
irep_idt  sval,
const exprt guard 
)

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.

◆ add_axioms_for_constrain_characters()

std::pair<exprt, string_constraintst> add_axioms_for_constrain_characters ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

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
fresh_symbolgenerator of fresh symbols
fa function application with arguments: integer |s|, character pointer &s[0], string char_set_string, optional integers start and end
array_poolpool of arrays representing strings
Returns
integer expression whose value is zero

Definition at line 290 of file string_constraint_generator_main.cpp.

◆ add_axioms_for_contains()

std::pair<exprt, string_constraintst> add_axioms_for_contains ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

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
    fresh_symbolgenerator of fresh symbols
    ffunction application with arguments refined_string s0 refined_string s1
    array_poolpool of arrays representing strings
    Returns
    Boolean expression contains

Definition at line 233 of file string_constraint_generator_testing.cpp.

◆ add_axioms_for_copy()

std::pair<exprt, string_constraintst> add_axioms_for_copy ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

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

Deprecated:
should use substring instead
Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with one argument, which is a string, or three arguments: string, integer offset and count
array_poolpool of arrays representing strings
Returns
a new string expression

Definition at line 490 of file string_constraint_generator_main.cpp.

◆ add_axioms_for_correct_number_format()

string_constraintst add_axioms_for_correct_number_format ( const array_string_exprt str,
const exprt radix_as_char,
const unsigned long  radix_ul,
const std::size_t  max_size,
const bool  strict_formatting 
)

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

Parameters
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 329 of file string_constraint_generator_valueof.cpp.

◆ add_axioms_for_cprover_string()

std::pair<exprt, string_constraintst> add_axioms_for_cprover_string ( symbol_generatort fresh_symbol,
const array_string_exprt res,
const exprt arg,
const exprt guard 
)

Convert an expression of type string_typet to a string_exprt.

Parameters
fresh_symbolgenerator of fresh symbols
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 82 of file string_constraint_generator_constants.cpp.

◆ add_axioms_for_delete() [1/2]

std::pair<exprt, string_constraintst> add_axioms_for_delete ( symbol_generatort fresh_symbol,
const array_string_exprt res,
const array_string_exprt str,
const exprt start,
const exprt end,
array_poolt array_pool 
)

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
fresh_symbolgenerator of fresh symbols
resarray of characters expression
strarray of characters expression
startinteger expression
endinteger expression
array_poolpool of arrays representing strings
Returns
integer expression different from zero to signal an exception

Definition at line 374 of file string_constraint_generator_transformation.cpp.

◆ add_axioms_for_delete() [2/2]

std::pair<exprt, string_constraintst> add_axioms_for_delete ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

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
fresh_symbolgenerator of fresh symbols
ffunction application with arguments integer |res|, character pointer &res[0], refined_string str, integer start and integer end
array_poolpool of arrays representing strings
Returns
an integer expression whose value is different from 0 to signal an exception

Definition at line 412 of file string_constraint_generator_transformation.cpp.

◆ add_axioms_for_delete_char_at()

std::pair<exprt, string_constraintst> add_axioms_for_delete_char_at ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

add axioms corresponding to the StringBuilder.deleteCharAt java function

Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with two arguments, the first is a string and the second is an index
array_poolpool of arrays representing strings
Returns
an expression whose value is non null to signal an exception

Definition at line 339 of file string_constraint_generator_transformation.cpp.

◆ add_axioms_for_empty_string()

std::pair<exprt, string_constraintst> add_axioms_for_empty_string ( const function_application_exprt f)

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

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

Definition at line 63 of file string_constraint_generator_constants.cpp.

◆ add_axioms_for_equals()

std::pair<exprt, string_constraintst> add_axioms_for_equals ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt pool 
)

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
    fresh_symbolgenerator of fresh symbols
    ffunction application with arguments refined_string s1 and refined_string s2
    poolpool of arrays representing strings
    Returns
    Boolean expression eq

Definition at line 31 of file string_constraint_generator_comparison.cpp.

◆ add_axioms_for_equals_ignore_case()

std::pair<exprt, string_constraintst> add_axioms_for_equals_ignore_case ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt pool 
)

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
    fresh_symbolgenerator of fresh symbols
    ffunction application with arguments refined_string s1 and refined_string s2
    poolpool of arrays representing strings
    Returns
    Boolean expression eq

Definition at line 132 of file string_constraint_generator_comparison.cpp.

◆ add_axioms_for_format() [1/2]

std::pair<exprt, string_constraintst> add_axioms_for_format ( symbol_generatort fresh_symbol,
const array_string_exprt res,
const std::string &  s,
const exprt::operandst args,
array_poolt array_pool,
const messaget message,
const namespacet ns 
)

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

Parameters
fresh_symbolgenerator of fresh symbols
resstring expression for the result of the format function
sa format string
argsa vector of arguments
array_poolpool of arrays representing strings
messagemessage handler for warnings
nsnamespace
Returns
code, 0 on success

Definition at line 381 of file string_constraint_generator_format.cpp.

◆ add_axioms_for_format() [2/2]

std::pair<exprt, string_constraintst> add_axioms_for_format ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool,
const messaget message,
const namespacet ns 
)

Formatted string using a format string and list of arguments.

Add axioms to specify the Java String.format function.

Parameters
fresh_symbolgenerator of fresh symbols
fa function application
array_poolpool of arrays representing strings
messagemessage handler for warnings
nsnamespace
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 510 of file string_constraint_generator_format.cpp.

◆ add_axioms_for_fractional_part()

std::pair<exprt, string_constraintst> add_axioms_for_fractional_part ( const array_string_exprt res,
const exprt int_expr,
size_t  max_size 
)

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 255 of file string_constraint_generator_float.cpp.

◆ add_axioms_for_index_of() [1/2]

std::pair<exprt, string_constraintst> add_axioms_for_index_of ( symbol_generatort fresh_symbol,
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.

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
    fresh_symbolgenerator of fresh symbols
    stran array of characters expression
    ca character expression
    from_indexan integer expression
    Returns
    integer expression index

Definition at line 38 of file string_constraint_generator_indexof.cpp.

◆ add_axioms_for_index_of() [2/2]

std::pair<exprt, string_constraintst> add_axioms_for_index_of ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

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
fresh_symbolgenerator of fresh symbols
ffunction application with arguments refined_string haystack, refined_string or character needle, and optional integer from_index with default value 0
array_poolpool of arrays representing strings
Returns
integer expression

Definition at line 291 of file string_constraint_generator_indexof.cpp.

◆ add_axioms_for_index_of_string()

std::pair<exprt, string_constraintst> add_axioms_for_index_of_string ( symbol_generatort fresh_symbol,
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.

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
    fresh_symbolgenerator of fresh symbols
    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 111 of file string_constraint_generator_indexof.cpp.

◆ add_axioms_for_insert() [1/2]

std::pair<exprt, string_constraintst> add_axioms_for_insert ( symbol_generatort fresh_symbol,
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
    fresh_symbolgenerator of fresh symbols
    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 33 of file string_constraint_generator_insert.cpp.

◆ add_axioms_for_insert() [2/2]

std::pair<exprt, string_constraintst> add_axioms_for_insert ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt pool 
)

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
fresh_symbolgenerator of fresh symbols
ffunction application with arguments integer |res|, character pointer &res[0], refined_string s1, refined_strings2, integer offset, optional integer start and optional integer end
poolpool of arrays representing strings
Returns
an integer expression which is different from zero if there is an exception to signal

Definition at line 106 of file string_constraint_generator_insert.cpp.

◆ add_axioms_for_insert_bool()

std::pair<exprt, string_constraintst> add_axioms_for_insert_bool ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

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

Deprecated:
should convert the value to string and call insert
Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with three arguments: a string, an integer offset, and a Boolean
array_poolpool of arrays representing strings
Returns
a new string expression

Definition at line 171 of file string_constraint_generator_insert.cpp.

◆ add_axioms_for_insert_char()

std::pair<exprt, string_constraintst> add_axioms_for_insert_char ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

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

Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with three arguments: a string, an integer offset, and a character
array_poolpool of arrays representing strings
Returns
an expression

Definition at line 196 of file string_constraint_generator_insert.cpp.

◆ add_axioms_for_insert_double()

std::pair<exprt, string_constraintst> add_axioms_for_insert_double ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool,
const namespacet ns 
)

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

Deprecated:
should convert the value to string and call insert
Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with three arguments: a string, an integer offset, and a double
array_poolpool of arrays representing strings
nsnamespace
Returns
a string expression

Definition at line 223 of file string_constraint_generator_insert.cpp.

◆ add_axioms_for_insert_float()

std::pair<exprt, string_constraintst> add_axioms_for_insert_float ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool,
const namespacet ns 
)

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

Deprecated:
should convert the value to string and call insert
Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with three arguments: a string, an integer offset, and a float
array_poolpool of arrays representing strings
nsnamespace
Returns
a new string expression

Definition at line 252 of file string_constraint_generator_insert.cpp.

◆ add_axioms_for_insert_int()

std::pair<exprt, string_constraintst> add_axioms_for_insert_int ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool,
const namespacet ns 
)

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

Deprecated:
should convert the value to string and call insert
Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with three arguments: a string, an integer offset, and an integer
array_poolpool of arrays representing strings
nsnamespace
Returns
an expression

Definition at line 144 of file string_constraint_generator_insert.cpp.

◆ add_axioms_for_is_empty()

std::pair<exprt, string_constraintst> add_axioms_for_is_empty ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

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
fresh_symbolgenerator of fresh symbols
ffunction application with a string argument
array_poolpool of arrays representing strings
Returns
a Boolean expression

Definition at line 126 of file string_constraint_generator_testing.cpp.

◆ add_axioms_for_is_prefix() [1/2]

std::pair<exprt, string_constraintst> add_axioms_for_is_prefix ( symbol_generatort fresh_symbol,
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.

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
fresh_symbolgenerator of fresh symbols
prefixan array of characters
stran array of characters
offsetan integer
Returns
Boolean expression isprefix

Definition at line 37 of file string_constraint_generator_testing.cpp.

◆ add_axioms_for_is_prefix() [2/2]

std::pair<exprt, string_constraintst> add_axioms_for_is_prefix ( symbol_generatort fresh_symbol,
const function_application_exprt f,
bool  swap_arguments,
array_poolt array_pool 
)

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
fresh_symbolgenerator of fresh symbols
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
array_poolpool of arrays representing strings
Returns
boolean expression isprefix

Definition at line 99 of file string_constraint_generator_testing.cpp.

◆ add_axioms_for_is_suffix()

std::pair<exprt, string_constraintst> add_axioms_for_is_suffix ( symbol_generatort fresh_symbol,
const function_application_exprt f,
bool  swap_arguments,
array_poolt array_pool 
)

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
fresh_symbolgenerator of fresh symbols
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
array_poolpool of arrays representing strings
Returns
Boolean expression issuffix

Definition at line 168 of file string_constraint_generator_testing.cpp.

◆ add_axioms_for_last_index_of() [1/2]

std::pair<exprt, string_constraintst> add_axioms_for_last_index_of ( symbol_generatort fresh_symbol,
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.

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
    fresh_symbolgenerator of fresh symbols
    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 346 of file string_constraint_generator_indexof.cpp.

◆ add_axioms_for_last_index_of() [2/2]

std::pair<exprt, string_constraintst> add_axioms_for_last_index_of ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

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
fresh_symbolgenerator of fresh symbols
ffunction application with arguments refined_string haystack, refined_string or character needle, and optional integer from_index with default value |haystack|-1
array_poolpool of arrays representing strings
Returns
an integer expression

Definition at line 415 of file string_constraint_generator_indexof.cpp.

◆ add_axioms_for_last_index_of_string()

std::pair<exprt, string_constraintst> add_axioms_for_last_index_of_string ( symbol_generatort fresh_symbol,
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.

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
    fresh_symbolgenerator of fresh symbols
    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 205 of file string_constraint_generator_indexof.cpp.

◆ add_axioms_for_length()

std::pair<exprt, string_constraintst> add_axioms_for_length ( const function_application_exprt f,
array_poolt array_pool 
)

Length of a string.

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

Parameters
ffunction application with argument string str
array_poolpool of arrays representing strings
Returns
expression |str|

Definition at line 513 of file string_constraint_generator_main.cpp.

◆ add_axioms_for_offset_by_code_point()

std::pair<exprt, string_constraintst> add_axioms_for_offset_by_code_point ( symbol_generatort fresh_symbol,
const function_application_exprt f 
)

Add axioms corresponding the String.offsetByCodePointCount java function.

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

Add axioms corresponding the String.offsetByCodePointCount java function.

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

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

Definition at line 222 of file string_constraint_generator_code_points.cpp.

◆ add_axioms_for_parse_int()

std::pair<exprt, string_constraintst> add_axioms_for_parse_int ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool,
const namespacet ns 
)

Integer value represented by a string.

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

Parameters
fresh_symbolgenerator of fresh symbols
fa function application with arguments refined_string str and an optional integer for the radix
array_poolpool of arrays representing strings
nsnamespace
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 507 of file string_constraint_generator_valueof.cpp.

◆ add_axioms_for_replace()

std::pair<exprt, string_constraintst> add_axioms_for_replace ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

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
    fresh_symbolgenerator of fresh symbols
    ffunction application with arguments integer |res|, character pointer &res[0], refined_string str, character old_char and character new_char
    array_poolpool of arrays representing strings
    Returns
    an integer expression equal to 0

Definition at line 297 of file string_constraint_generator_transformation.cpp.

◆ add_axioms_for_set_length()

std::pair<exprt, string_constraintst> add_axioms_for_set_length ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

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
    fresh_symbolgenerator of fresh symbols
    ffunction application with arguments integer |res|, character pointer &res[0], refined_string s1, integer k
    array_poolpool of arrays representing strings
    Returns
    integer expression equal to 0

Definition at line 37 of file string_constraint_generator_transformation.cpp.

◆ add_axioms_for_string_of_float() [1/2]

std::pair<exprt, string_constraintst> add_axioms_for_string_of_float ( symbol_generatort fresh_symbol,
const array_string_exprt res,
const exprt f,
array_poolt array_pool,
const namespacet ns 
)

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
fresh_symbolgenerator of fresh symbols
resstring expression corresponding to the result
fa float expression, which is positive
array_poolpool of arrays representing strings
nsnamespace
Returns
an integer expression, different from zero if an error should be raised

Definition at line 201 of file string_constraint_generator_float.cpp.

◆ add_axioms_for_string_of_float() [2/2]

std::pair<exprt, string_constraintst> add_axioms_for_string_of_float ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool,
const namespacet ns 
)

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
fresh_symbolgenerator of fresh symbols
ffunction application with one float argument
array_poolpool of arrays representing strings
nsnamespace
Returns
an integer expression

Definition at line 158 of file string_constraint_generator_float.cpp.

◆ add_axioms_for_string_of_int()

std::pair<exprt, string_constraintst> add_axioms_for_string_of_int ( const array_string_exprt res,
const exprt input_int,
size_t  max_size,
const namespacet ns 
)

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")
nsnamespace
Returns
code 0 on success

Definition at line 132 of file string_constraint_generator_valueof.cpp.

◆ add_axioms_for_string_of_int_with_radix()

std::pair<exprt, string_constraintst> add_axioms_for_string_of_int_with_radix ( const array_string_exprt res,
const exprt input_int,
const exprt radix,
size_t  max_size,
const namespacet ns 
)

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")
nsnamespace
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 153 of file string_constraint_generator_valueof.cpp.

◆ add_axioms_for_substring() [1/2]

std::pair<exprt, string_constraintst> add_axioms_for_substring ( symbol_generatort fresh_symbol,
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')`.

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
    fresh_symbolgenerator of fresh symbols
    resarray of characters expression
    strarray of characters expression
    startinteger expression
    endinteger expression
    Returns
    integer expression equal to zero

Definition at line 124 of file string_constraint_generator_transformation.cpp.

◆ add_axioms_for_substring() [2/2]

std::pair<exprt, string_constraintst> add_axioms_for_substring ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

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
fresh_symbolgenerator of fresh symbols
ffunction application with arguments integer |res|, character pointer &res[0], refined_string str, integer start, optional integer end with default value |str|.
array_poolpool of arrays representing strings
Returns
integer expression which is different from 0 when there is an exception to signal

Definition at line 94 of file string_constraint_generator_transformation.cpp.

◆ add_axioms_for_trim()

std::pair<exprt, string_constraintst> add_axioms_for_trim ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

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
    fresh_symbolgenerator of fresh symbols
    ffunction application with arguments integer |res|, character pointer &res[0], refined_string str.
    array_poolpool of arrays representing strings
    Returns
    integer expression which is different from 0 when there is an exception to signal

Definition at line 183 of file string_constraint_generator_transformation.cpp.

◆ add_axioms_from_bool() [1/2]

std::pair<exprt, string_constraintst> add_axioms_from_bool ( const array_string_exprt res,
const exprt b 
)

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 83 of file string_constraint_generator_valueof.cpp.

◆ add_axioms_from_bool() [2/2]

std::pair<exprt, string_constraintst> add_axioms_from_bool ( const function_application_exprt f,
array_poolt array_pool 
)

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
array_poolpool of arrays representing strings
Returns
a new string expression

Definition at line 66 of file string_constraint_generator_valueof.cpp.

◆ add_axioms_from_char() [1/2]

std::pair<exprt, string_constraintst> add_axioms_from_char ( const array_string_exprt res,
const exprt c 
)

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 311 of file string_constraint_generator_valueof.cpp.

◆ add_axioms_from_char() [2/2]

std::pair<exprt, string_constraintst> add_axioms_from_char ( const function_application_exprt f,
array_poolt array_pool 
)

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
array_poolpool of arrays representing strings
Returns
code 0 on success

Definition at line 294 of file string_constraint_generator_valueof.cpp.

◆ add_axioms_from_double()

std::pair<exprt, string_constraintst> add_axioms_from_double ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool,
const namespacet ns 
)

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

Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with one double argument
array_poolpool of arrays representing strings
nsnamespace
Returns
an integer expression

Definition at line 177 of file string_constraint_generator_float.cpp.

◆ add_axioms_from_float_scientific_notation() [1/2]

std::pair<exprt, string_constraintst> add_axioms_from_float_scientific_notation ( symbol_generatort fresh_symbol,
const array_string_exprt res,
const exprt f,
array_poolt array_pool,
const namespacet ns 
)

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
fresh_symbolgenerator of fresh symbols
resstring expression representing the float in scientific notation
fa float expression, which is positive
array_poolpool of arrays representing strings
nsnamespace
Returns
a integer expression different from 0 to signal an exception

Definition at line 344 of file string_constraint_generator_float.cpp.

◆ add_axioms_from_float_scientific_notation() [2/2]

std::pair<exprt, string_constraintst> add_axioms_from_float_scientific_notation ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool,
const namespacet ns 
)

Representation of a float value in scientific notation.

Add axioms corresponding to the scientific representation of floating point values

Parameters
fresh_symbolgenerator of fresh symbols
fa function application expression
array_poolpool of arrays representing strings
nsnamespace
Returns
code 0 on success

Definition at line 540 of file string_constraint_generator_float.cpp.

◆ add_axioms_from_int_hex() [1/2]

std::pair<exprt, string_constraintst> add_axioms_from_int_hex ( const array_string_exprt res,
const exprt i 
)

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

Deprecated:
use add_axioms_from_int_with_radix instead
Parameters
resstring expression for the result
ian integer argument
Returns
code 0 on success

Definition at line 216 of file string_constraint_generator_valueof.cpp.

◆ add_axioms_from_int_hex() [2/2]

std::pair<exprt, string_constraintst> add_axioms_from_int_hex ( const function_application_exprt f,
array_poolt array_pool 
)

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

Parameters
ffunction application with an integer argument
array_poolpool of arrays representing strings
Returns
code 0 on success

Definition at line 273 of file string_constraint_generator_valueof.cpp.

◆ add_axioms_from_literal()

std::pair<exprt, string_constraintst> add_axioms_from_literal ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

String corresponding to an internal cprover string.

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

Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with an argument which is a string literal that is a constant with a string value.
array_poolpool of arrays representing strings
Returns
string expression

Definition at line 114 of file string_constraint_generator_constants.cpp.

◆ add_axioms_from_long()

std::pair<exprt, string_constraintst> add_axioms_from_long ( const function_application_exprt f,
array_poolt array_pool,
const namespacet ns 
)

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
array_poolpool of arrays representing strings
nsnamespace
Returns
a new string expression

Definition at line 45 of file string_constraint_generator_valueof.cpp.

◆ add_constraint_on_characters()

string_constraintst add_constraint_on_characters ( symbol_generatort fresh_symbol,
const array_string_exprt s,
const exprt start,
const exprt end,
const std::string &  char_set 
)

Add constraint on characters of a string.

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

Parameters
fresh_symbolgenerator of fresh symbols
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 254 of file string_constraint_generator_main.cpp.

◆ char_array_of_pointer()

const array_string_exprt& char_array_of_pointer ( array_poolt pool,
const exprt pointer,
const exprt length 
)

Adds creates a new array if it does not already exists.

Definition at line 325 of file string_constraint_generator_main.cpp.

◆ combine_results()

std::pair<exprt, string_constraintst> combine_results ( std::pair< exprt, string_constraintst result1,
std::pair< exprt, string_constraintst result2 
)

Combine the results of two add_axioms function by taking the maximum of the return codes and merging the constraints.

Definition at line 598 of file string_constraint_generator_main.cpp.

◆ get_numeric_value_from_character()

exprt get_numeric_value_from_character ( const exprt chr,
const typet char_type,
const typet type,
const bool  strict_formatting,
const unsigned long  radix_ul 
)

Get the numeric value of a character, assuming that the radix is large enough.

'+' and '-' yield 0.

Parameters
chrthe character to get the numeric value of
char_typethe type to use for characters
typethe type to use for the return value
strict_formattingif true, don't allow upper case characters
radix_ulthe radix, which should be between 2 and 36, or 0, in which case the return value will work for any radix
Returns
an integer expression of the given type with the numeric value of the char

There are four cases, which occur in ASCII in the following order: '+' and '-', digits, upper case letters, lower case letters

return char >= '0' ? (char - '0') : 0

return char >= 'a' ? (char - 'a' + 10) : char >= '0' ? (char - '0') : 0

return char >= 'a' ? (char - 'a' + 10) : char >= 'A' ? (char - 'A' + 10) : char >= '0' ? (char - '0') : 0

Definition at line 630 of file string_constraint_generator_valueof.cpp.

◆ get_return_code_type()

signedbv_typet get_return_code_type ( )

Definition at line 339 of file string_constraint_generator_main.cpp.

◆ get_string_expr()

array_string_exprt get_string_expr ( array_poolt pool,
const exprt expr 
)

casts an expression to a string expression, or fetches the actual string_exprt in the case of a symbol.

Parameters
poolpool of arrays representing strings
expran expression of refined string type
Returns
a string expression

Definition at line 210 of file string_constraint_generator_main.cpp.

◆ is_digit_with_radix()

exprt is_digit_with_radix ( const exprt chr,
const bool  strict_formatting,
const exprt radix_as_char,
const unsigned long  radix_ul 
)

Check if a character is a digit with respect to the given radix, e.g.

if the radix is 10 then check if the character is in the range 0-9.

Parameters
chrthe character
strict_formattingif true, don't allow upper case characters
radix_as_charthe radix as an expression of the same type as chr
radix_ulthe radix, which should be between 2 and 36, or 0, in which case the return value will work for any radix
Returns
an expression for the condition

Definition at line 560 of file string_constraint_generator_valueof.cpp.

◆ is_positive()

exprt is_positive ( const exprt x)
Parameters
xan expression
Returns
a Boolean expression true exactly when x is positive

Definition at line 524 of file string_constraint_generator_main.cpp.

◆ length_constraint_for_concat()

exprt length_constraint_for_concat ( const array_string_exprt res,
const array_string_exprt s1,
const array_string_exprt s2 
)

Add axioms enforcing that the length of res is that of the concatenation of s1 with s2

Definition at line 99 of file string_constraint_generator_concat.cpp.

◆ length_constraint_for_concat_char()

exprt length_constraint_for_concat_char ( const array_string_exprt res,
const array_string_exprt s1 
)

Add axioms enforcing that the length of res is that of the concatenation of s1 with.

Definition at line 109 of file string_constraint_generator_concat.cpp.

◆ length_constraint_for_concat_substr()

exprt length_constraint_for_concat_substr ( const array_string_exprt res,
const array_string_exprt s1,
const array_string_exprt s2,
const exprt start,
const exprt end 
)

Add axioms enforcing that the length of res is that of the concatenation of s1 with the substring of s2 starting at index ‘start’ and ending at indexend'‘.

Where start_index’ is max(0, start) and end' is max(min(end, s2.length), start')

Definition at line 81 of file string_constraint_generator_concat.cpp.

◆ length_constraint_for_insert()

exprt length_constraint_for_insert ( const array_string_exprt res,
const array_string_exprt s1,
const array_string_exprt s2 
)

Add axioms ensuring the length of res corresponds to that of s1 where we inserted s2.

Definition at line 80 of file string_constraint_generator_insert.cpp.

◆ max_printed_string_length()

size_t max_printed_string_length ( const typet type,
unsigned long  radix_ul 
)

Calculate the string length needed to represent any value of the given type using the given radix.

Due to floating point rounding errors we sometimes return a value 1 larger than needed, which is fine for our purposes.

Parameters
typethe type that we are considering values of
radix_ulthe radix we are using, or 0, in which case the return value will work for any radix
Returns
the maximum string length

We want to calculate max, the maximum number of characters needed to represent any value of the given type.

For signed types, the longest string will be for -2^(n_bits-1), so max = 1 + min{k: 2^(n_bits-1) < radix^k} (the 1 is for the minus sign) = 1 + min{k: n_bits-1 < k log_2(radix)} = 1 + min{k: k > (n_bits-1) / log_2(radix)} = 1 + min{k: k > floor((n_bits-1) / log_2(radix))} = 1 + (1 + floor((n_bits-1) / log_2(radix))) = 2 + floor((n_bits-1) / log_2(radix))

For unsigned types, the longest string will be for (2^n_bits)-1, so max = min{k: (2^n_bits)-1 < radix^k} = min{k: 2^n_bits <= radix^k} = min{k: n_bits <= k log_2(radix)} = min{k: k >= n_bits / log_2(radix)} = min{k: k >= ceil(n_bits / log_2(radix))} = ceil(n_bits / log_2(radix))

Definition at line 704 of file string_constraint_generator_valueof.cpp.

◆ maximum()

exprt maximum ( const exprt a,
const exprt b 
)
Returns
expression representing the maximum of two expressions

Definition at line 583 of file string_constraint_generator_main.cpp.

◆ merge()

void merge ( string_constraintst result,
string_constraintst  other 
)

Merge two sets of constraints by appending to the first one.

Definition at line 225 of file string_constraint_generator_main.cpp.

◆ minimum()

exprt minimum ( const exprt a,
const exprt b 
)
Returns
expression representing the minimum of two expressions

Definition at line 578 of file string_constraint_generator_main.cpp.

◆ of_argument()

array_string_exprt of_argument ( array_poolt array_pool,
const exprt arg 
)

Converts a struct containing a length and pointer to an array.

This allows to get a string expression from arguments of a string builtion function, because string arguments in these function calls are given as a struct containing a length and pointer to an array.

Definition at line 333 of file string_constraint_generator_main.cpp.

◆ sum_overflows()

exprt sum_overflows ( const plus_exprt sum)
Returns
Boolean true when the sum of the two expressions overflows

Definition at line 54 of file string_constraint_generator_main.cpp.

◆ utf16_constant_array_to_java()

std::string utf16_constant_array_to_java ( const array_exprt arr,
std::size_t  length 
)

Construct a string from a constant array.

Parameters
arran array expression containing only constants
lengthan unsigned value representing the length of the array
Returns
String of length length represented by the array assuming each field in arr represents a character.

Definition at line 483 of file string_constraint_generator_format.cpp.

◆ zero_if_negative()

exprt zero_if_negative ( const exprt expr)

Returns a non-negative version of the argument.

Parameters
exprexpression of which we want a non-negative version
Returns
max(0, expr)

Definition at line 591 of file string_constraint_generator_main.cpp.