cprover
string_constraint_generator_comparison.cpp File Reference

Generates string constraints for function comparing strings, such as: equals, equalsIgnoreCase, compareTo, hashCode, intern. More...

+ Include dependency graph for string_constraint_generator_comparison.cpp:

Go to the source code of this file.

Functions

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...
 
static exprt character_equals_ignore_case (const exprt &char1, const exprt &char2, const exprt &char_a, const exprt &char_A, const exprt &char_Z)
 Returns an expression which is true when the two given characters are equal when ignoring case for ASCII. 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_compare_to (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool)
 Lexicographic comparison of two strings. More...
 

Detailed Description

Generates string constraints for function comparing strings, such as: equals, equalsIgnoreCase, compareTo, hashCode, intern.

Definition in file string_constraint_generator_comparison.cpp.

Function Documentation

◆ 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_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.

◆ character_equals_ignore_case()

static exprt character_equals_ignore_case ( const exprt char1,
const exprt char2,
const exprt char_a,
const exprt char_A,
const exprt char_Z 
)
static

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

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

Definition at line 87 of file string_constraint_generator_comparison.cpp.