CBMC
string_constraint_generatort Class Referencefinal

#include <string_constraint_generator.h>

+ Collaboration diagram for string_constraint_generatort:

Classes

struct  parseint_argumentst
 Argument block for parseInt and cousins, common to parseInt itself and CProverString.isValidInt. More...
 

Public Member Functions

 string_constraint_generatort (const namespacet &ns, message_handlert &message_handler)
 
std::pair< exprt, string_constraintstadd_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...
 
std::optional< exprtmake_array_pointer_association (const exprt &return_code, const function_application_exprt &expr)
 Associate array to pointer, and array to length. More...
 
std::pair< exprt, string_constraintstadd_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...
 
std::pair< exprt, string_constraintstadd_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...
 
std::pair< exprt, string_constraintstadd_axioms_for_insert (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &offset)
 
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)
 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 (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 (const function_application_exprt &f)
 Add axioms to ensure all characters of a string belong to a given set. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_char_at (const function_application_exprt &f)
 Character at a given position. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_code_point_at (const function_application_exprt &f)
 add axioms corresponding to the String.codePointAt java function More...
 
std::pair< exprt, string_constraintstadd_axioms_for_code_point_before (const function_application_exprt &f)
 add axioms corresponding to the String.codePointBefore java function More...
 
std::pair< exprt, string_constraintstadd_axioms_for_contains (const function_application_exprt &f)
 Test whether a string contains another. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_equals (const function_application_exprt &f)
 Equality of the content of two strings. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_equals_ignore_case (const function_application_exprt &f)
 Equality of the content ignoring case of characters. More...
 
std::pair< exprt, string_constraintstadd_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...
 
std::pair< exprt, string_constraintstadd_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...
 
std::pair< exprt, string_constraintstadd_axioms_for_is_prefix (const function_application_exprt &f, bool swap_arguments)
 Test if the target is a prefix of the string. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_is_suffix (const function_application_exprt &f, bool swap_arguments)
 Test if the target is a suffix of the string. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_length (const function_application_exprt &f)
 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 (const function_application_exprt &f)
 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 (const function_application_exprt &f)
 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 (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...
 
std::pair< exprt, string_constraintstadd_axioms_for_delete (const function_application_exprt &f)
 Remove a portion of a string. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_delete_char_at (const function_application_exprt &expr)
 add axioms corresponding to the StringBuilder.deleteCharAt java function More...
 
std::pair< exprt, string_constraintstadd_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...
 
std::pair< exprt, string_constraintstadd_axioms_from_literal (const function_application_exprt &f)
 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)
 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)
 Add axioms corresponding to the Integer.toHexString(I) java function. More...
 
std::pair< exprt, string_constraintstadd_axioms_from_long (const function_application_exprt &f)
 Add axioms corresponding to the String.valueOf(J) java function. More...
 
std::pair< exprt, string_constraintstadd_axioms_from_bool (const function_application_exprt &f)
 
std::pair< exprt, string_constraintstadd_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. More...
 
std::pair< exprt, string_constraintstadd_axioms_from_char (const function_application_exprt &f)
 
std::pair< exprt, string_constraintstadd_axioms_from_char (const array_string_exprt &res, const exprt &c)
 
std::pair< exprt, string_constraintstadd_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...
 
std::pair< exprt, string_constraintstadd_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...
 
std::pair< exprt, string_constraintstadd_axioms_for_index_of (const function_application_exprt &f)
 Index of the first occurence of a target inside the string. More...
 
std::pair< exprt, string_constraintstadd_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...
 
std::pair< exprt, string_constraintstadd_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...
 
std::pair< exprt, string_constraintstadd_axioms_for_last_index_of (const function_application_exprt &f)
 Index of the last occurence of a target inside the string. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_string_of_float (const function_application_exprt &f)
 String representation of a float value. More...
 
std::pair< exprt, string_constraintstadd_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...
 
std::pair< exprt, string_constraintstadd_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. More...
 
std::pair< exprt, string_constraintstadd_axioms_from_float_scientific_notation (const array_string_exprt &res, const exprt &f)
 Add axioms to write the float in scientific notation. More...
 
std::pair< exprt, string_constraintstadd_axioms_from_float_scientific_notation (const function_application_exprt &f)
 Representation of a float value in scientific notation. More...
 
std::pair< exprt, string_constraintstadd_axioms_from_double (const function_application_exprt &f)
 Add axioms corresponding to the String.valueOf(D) java function. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_replace (const function_application_exprt &f)
 Replace a character by another in a string. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_set_length (const function_application_exprt &f)
 Reduce or extend a string to have the given length. More...
 
std::pair< exprt, string_constraintstadd_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...
 
std::pair< exprt, string_constraintstadd_axioms_for_substring (const function_application_exprt &f)
 Substring of a string between two indices. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_trim (const function_application_exprt &f)
 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 (const function_application_exprt &f)
 Add axioms corresponding the String.codePointCount java function. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_offset_by_code_point (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...
 
std::vector< exprtget_conjuncts_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 (const function_application_exprt &f)
 Integer value represented by a string. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_is_valid_int (const function_application_exprt &f)
 Check a string is a valid integer, using the same rules as Java Integer.parseInt. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_compare_to (const function_application_exprt &f)
 Lexicographic comparison of two strings. 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...
 
parseint_argumentst unpack_parseint_arguments (const function_application_exprt &f, const typet &target_int_type)
 

Public Attributes

symbol_generatort fresh_symbol
 
array_poolt array_pool
 
const namespacet ns
 

Private Member Functions

exprt associate_array_to_pointer (const exprt &return_code, const function_application_exprt &f)
 Associate a char array to a char pointer. More...
 
exprt associate_length_to_array (const exprt &return_code, const function_application_exprt &f)
 Associate an integer length to a char array. More...
 

Private Attributes

message_handlertmessage_handler
 

Detailed Description

Definition at line 47 of file string_constraint_generator.h.

Constructor & Destructor Documentation

◆ string_constraint_generatort()

string_constraint_generatort::string_constraint_generatort ( const namespacet ns,
message_handlert message_handler 
)

Definition at line 33 of file string_constraint_generator_main.cpp.

Member Function Documentation

◆ add_axioms_for_char_at()

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

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 387 of file string_constraint_generator_main.cpp.

◆ add_axioms_for_char_literal()

std::pair< exprt, string_constraintst > string_constraint_generatort::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 350 of file string_constraint_generator_main.cpp.

◆ add_axioms_for_characters_in_integer_string()

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

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

◆ add_axioms_for_code_point()

std::pair< exprt, string_constraintst > string_constraint_generatort::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 23 of file string_constraint_generator_code_points.cpp.

◆ add_axioms_for_code_point_at()

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

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

◆ add_axioms_for_code_point_before()

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

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

◆ add_axioms_for_code_point_count()

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

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.

"deprecated since " "2017" "-" "10" "-" "5" "; " "Java specific, 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 191 of file string_constraint_generator_code_points.cpp.

◆ add_axioms_for_compare_to()

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

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 209 of file string_constraint_generator_comparison.cpp.

◆ add_axioms_for_concat()

std::pair< exprt, string_constraintst > 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 160 of file string_concatenation_builtin_function.cpp.

◆ add_axioms_for_concat_code_point()

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

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 175 of file string_concatenation_builtin_function.cpp.

◆ add_axioms_for_concat_substr()

std::pair< exprt, string_constraintst > 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 53 of file string_concatenation_builtin_function.cpp.

◆ add_axioms_for_constant()

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

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 > string_constraint_generatort::add_axioms_for_constrain_characters ( const function_application_exprt f)

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 163 of file string_constraint_generator_main.cpp.

◆ add_axioms_for_contains()

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

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 250 of file string_constraint_generator_testing.cpp.

◆ add_axioms_for_copy()

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

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
Deprecated:
"deprecated since " "2017" "-" "10" "-" "5" "; " "should use substring instead"

Definition at line 311 of file string_constraint_generator_main.cpp.

◆ add_axioms_for_cprover_string()

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

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

◆ add_axioms_for_delete() [1/2]

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

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 383 of file string_constraint_generator_transformation.cpp.

◆ add_axioms_for_delete() [2/2]

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

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 418 of file string_constraint_generator_transformation.cpp.

◆ add_axioms_for_delete_char_at()

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

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 356 of file string_constraint_generator_transformation.cpp.

◆ add_axioms_for_empty_string()

std::pair< exprt, string_constraintst > string_constraint_generatort::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 64 of file string_constraint_generator_constants.cpp.

◆ add_axioms_for_equals()

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

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 31 of file string_constraint_generator_comparison.cpp.

◆ add_axioms_for_equals_ignore_case()

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

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 136 of file string_constraint_generator_comparison.cpp.

◆ add_axioms_for_fractional_part()

std::pair< exprt, string_constraintst > string_constraint_generatort::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 245 of file string_constraint_generator_float.cpp.

◆ add_axioms_for_function_application()

std::pair< exprt, string_constraintst > 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
expran expression containing a function application
Returns
expression corresponding to the result of the function application

Definition at line 214 of file string_constraint_generator_main.cpp.

◆ add_axioms_for_index_of() [1/2]

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

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 41 of file string_constraint_generator_indexof.cpp.

◆ add_axioms_for_index_of() [2/2]

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

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 309 of file string_constraint_generator_indexof.cpp.

◆ add_axioms_for_index_of_string()

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

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 115 of file string_constraint_generator_indexof.cpp.

◆ add_axioms_for_insert()

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

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

Deprecated:
should use string_length(s)==0 instead
Parameters
ffunction application with a string argument
Returns
a Boolean expression
Deprecated:
"deprecated since " "2017" "-" "10" "-" "5" "; " "should use `string_length s == 0` instead"

Definition at line 130 of file string_constraint_generator_testing.cpp.

◆ add_axioms_for_is_prefix() [1/2]

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

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 38 of file string_constraint_generator_testing.cpp.

◆ add_axioms_for_is_prefix() [2/2]

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_is_prefix ( const function_application_exprt f,
bool  swap_arguments 
)

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 offsetwhose 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 106 of file string_constraint_generator_testing.cpp.

◆ add_axioms_for_is_suffix()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_is_suffix ( const function_application_exprt f,
bool  swap_arguments 
)

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
Deprecated:

Should use strings_startwith(s0, s1, s1.length - s0.length).

"deprecated since " "2018" "-" "6" "-" "6" "; " "should use strings_startwith"

Definition at line 171 of file string_constraint_generator_testing.cpp.

◆ add_axioms_for_is_valid_int()

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

Check a string is a valid integer, using the same rules as Java Integer.parseInt.

Add axioms relating a boolean return value to being a valid integer

Parameters
fa function application with arguments refined_string str and an optional integer for the radix
Returns
boolean expression indicating whether the string is a valid integer
Note
the only thing stopping us from taking longer strings with many leading zeros is the axioms for correct number format

Definition at line 489 of file string_constraint_generator_valueof.cpp.

◆ add_axioms_for_last_index_of() [1/2]

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

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 363 of file string_constraint_generator_indexof.cpp.

◆ add_axioms_for_last_index_of() [2/2]

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

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 433 of file string_constraint_generator_indexof.cpp.

◆ add_axioms_for_last_index_of_string()

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

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 216 of file string_constraint_generator_indexof.cpp.

◆ add_axioms_for_length()

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

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 331 of file string_constraint_generator_main.cpp.

◆ add_axioms_for_offset_by_code_point()

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

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.

"deprecated since " "2017" "-" "10" "-" "5" "; " "Java specific, 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 217 of file string_constraint_generator_code_points.cpp.

◆ add_axioms_for_parse_int()

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

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

Definition at line 525 of file string_constraint_generator_valueof.cpp.

◆ add_axioms_for_replace()

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

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 313 of file string_constraint_generator_transformation.cpp.

◆ add_axioms_for_set_length()

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

Reduce or extend a string to have the given length.

Add axioms ensuring the returned string expression res has length max(k, 0) 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. Note this means if k is negative then the string is truncated to length 0; in practice a wrapper function will usually handle this case.

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 expression equal to 0

Definition at line 39 of file string_constraint_generator_transformation.cpp.

◆ add_axioms_for_string_of_float() [1/2]

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

', 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
fa float expression, which is positive
Returns
an integer expression, different from zero if an error should be raised

Definition at line 193 of file string_constraint_generator_float.cpp.

◆ add_axioms_for_string_of_float() [2/2]

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

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

◆ add_axioms_for_string_of_int()

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

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

◆ add_axioms_for_string_of_int_with_radix()

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

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

◆ add_axioms_for_substring() [1/2]

std::pair< exprt, string_constraintst > string_constraint_generatort::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')`.

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 124 of file string_constraint_generator_transformation.cpp.

◆ add_axioms_for_substring() [2/2]

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

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 96 of file string_constraint_generator_transformation.cpp.

◆ add_axioms_for_trim()

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

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 183 of file string_constraint_generator_transformation.cpp.

◆ add_axioms_from_bool() [1/2]

std::pair< exprt, string_constraintst > string_constraint_generatort::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
Deprecated:
"deprecated since " "2017" "-" "10" "-" "5" "; " "Java specific, should be implemented in Java"

Definition at line 65 of file string_constraint_generator_valueof.cpp.

◆ add_axioms_from_bool() [2/2]

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

◆ add_axioms_from_char() [1/2]

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

◆ add_axioms_from_char() [2/2]

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

◆ add_axioms_from_double()

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

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

Parameters
ffunction application with one double argument
Returns
an integer expression

Definition at line 174 of file string_constraint_generator_float.cpp.

◆ add_axioms_from_float_scientific_notation() [1/2]

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_from_float_scientific_notation ( const array_string_exprt res,
const exprt float_expr 
)

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
float_expra float expression, which is positive
Returns
a integer expression different from 0 to signal an exception

Definition at line 338 of file string_constraint_generator_float.cpp.

◆ add_axioms_from_float_scientific_notation() [2/2]

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

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

◆ add_axioms_from_int_hex() [1/2]

std::pair< exprt, string_constraintst > string_constraint_generatort::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
Deprecated:
"deprecated since " "2017" "-" "10" "-" "5" "; " "use add_axioms_for_string_of_int_with_radix"

Definition at line 200 of file string_constraint_generator_valueof.cpp.

◆ add_axioms_from_int_hex() [2/2]

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

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

◆ add_axioms_from_literal()

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

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.

◆ add_axioms_from_long()

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

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
Deprecated:
"deprecated since " "2017" "-" "10" "-" "5" "; " "use add_axioms_for_string_of_int instead"

Definition at line 44 of file string_constraint_generator_valueof.cpp.

◆ add_constraint_on_characters()

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

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 129 of file string_constraint_generator_main.cpp.

◆ associate_array_to_pointer()

exprt string_constraint_generatort::associate_array_to_pointer ( const exprt return_code,
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
return_codeexpression which is assigned the result of the function
fa function application with argument a character array arr and a character pointer ptr.
Returns
a constraint

Definition at line 63 of file string_constraint_generator_main.cpp.

◆ associate_length_to_array()

exprt string_constraint_generatort::associate_length_to_array ( const exprt return_code,
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
return_codeexpression which is assigned the result of the function
fa function application with argument a character array arr and an integer length.
Returns
a constraint

Definition at line 87 of file string_constraint_generator_main.cpp.

◆ combine_results()

std::pair< exprt, string_constraintst > string_constraint_generatort::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 420 of file string_constraint_generator_main.cpp.

◆ get_conjuncts_for_correct_number_format()

std::vector< exprt > string_constraint_generatort::get_conjuncts_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 279 of file string_constraint_generator_valueof.cpp.

◆ make_array_pointer_association()

std::optional< exprt > string_constraint_generatort::make_array_pointer_association ( const exprt return_code,
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 196 of file string_constraint_generator_main.cpp.

◆ unpack_parseint_arguments()

string_constraint_generatort::parseint_argumentst string_constraint_generatort::unpack_parseint_arguments ( const function_application_exprt f,
const typet target_int_type 
)

Definition at line 458 of file string_constraint_generator_valueof.cpp.

Member Data Documentation

◆ array_pool

array_poolt string_constraint_generatort::array_pool

Definition at line 63 of file string_constraint_generator.h.

◆ fresh_symbol

symbol_generatort string_constraint_generatort::fresh_symbol

Definition at line 61 of file string_constraint_generator.h.

◆ message_handler

message_handlert& string_constraint_generatort::message_handler
private

Definition at line 75 of file string_constraint_generator.h.

◆ ns

const namespacet string_constraint_generatort::ns

Definition at line 65 of file string_constraint_generator.h.


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