cprover
string_constraint_generatort Class Referencefinal

#include <string_constraint_generator.h>

+ Collaboration diagram for string_constraint_generatort:

Public Member Functions

 string_constraint_generatort (const namespacet &ns)
 
std::pair< exprt, string_constraintstadd_axioms_for_function_application (symbol_generatort &fresh_symbol, const function_application_exprt &expr)
 strings contained in this call are converted to objects of type string_exprt, through adding axioms. More...
 
optionalt< exprtmake_array_pointer_association (const function_application_exprt &expr)
 Associate array to pointer, and array to length. More...
 

Public Attributes

symbol_generatort fresh_symbol
 
array_poolt array_pool
 
string_constraintst constraints
 
const namespacet ns
 

Private Member Functions

std::pair< symbol_exprt, string_constraintstadd_axioms_for_intern (symbol_generatort &fresh_symbol, const function_application_exprt &f)
 Add axioms corresponding to the String.intern java function. More...
 
exprt associate_array_to_pointer (const function_application_exprt &f)
 Associate a char array to a char pointer. More...
 
exprt associate_length_to_array (const function_application_exprt &f)
 Associate an integer length to a char array. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_hash_code (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool)
 Value that is identical for strings with the same content. More...
 

Private Attributes

const messaget message
 
std::map< array_string_exprt, exprthash_code_of_string
 
std::map< array_string_exprt, symbol_exprtintern_of_string
 

Detailed Description

Definition at line 120 of file string_constraint_generator.h.

Constructor & Destructor Documentation

◆ string_constraint_generatort()

string_constraint_generatort::string_constraint_generatort ( const namespacet ns)
explicit

Definition at line 32 of file string_constraint_generator_main.cpp.

Member Function Documentation

◆ add_axioms_for_function_application()

std::pair< exprt, string_constraintst > string_constraint_generatort::add_axioms_for_function_application ( symbol_generatort fresh_symbol,
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
fresh_symbolgenerator of fresh symbols
expran expression containing a function application
Returns
expression corresponding to the result of the function application

Definition at line 370 of file string_constraint_generator_main.cpp.

◆ add_axioms_for_hash_code()

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

Value that is identical for strings with the same content.

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

  • \( hash(str)=hash(s) \lor |str| \ne |s| \lor (|str|=|s| \land \exists i<|s|.\ s[i]\ne str[i]) \)
    Parameters
    fresh_symbolgenerator of fresh symbols
    ffunction application with argument refined_string str
    poolpool of arrays representing strings
    Returns
    integer expression hash(str)

Definition at line 190 of file string_constraint_generator_comparison.cpp.

◆ add_axioms_for_intern()

std::pair< symbol_exprt, string_constraintst > string_constraint_generatort::add_axioms_for_intern ( symbol_generatort fresh_symbol,
const function_application_exprt f 
)
private

Add axioms corresponding to the String.intern java function.

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

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

Definition at line 310 of file string_constraint_generator_comparison.cpp.

◆ associate_array_to_pointer()

exprt string_constraint_generatort::associate_array_to_pointer ( const function_application_exprt f)
private

Associate a char array to a char pointer.

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

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

Definition at line 171 of file string_constraint_generator_main.cpp.

◆ associate_length_to_array()

exprt string_constraint_generatort::associate_length_to_array ( const function_application_exprt f)
private

Associate an integer length to a char array.

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

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

Definition at line 193 of file string_constraint_generator_main.cpp.

◆ make_array_pointer_association()

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

Associate array to pointer, and array to length.

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

Definition at line 352 of file string_constraint_generator_main.cpp.

Member Data Documentation

◆ array_pool

array_poolt string_constraint_generatort::array_pool

Definition at line 135 of file string_constraint_generator.h.

◆ constraints

string_constraintst string_constraint_generatort::constraints

Definition at line 137 of file string_constraint_generator.h.

◆ fresh_symbol

symbol_generatort string_constraint_generatort::fresh_symbol

Definition at line 133 of file string_constraint_generator.h.

◆ hash_code_of_string

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

Definition at line 173 of file string_constraint_generator.h.

◆ intern_of_string

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

Definition at line 176 of file string_constraint_generator.h.

◆ message

const messaget string_constraint_generatort::message
private

Definition at line 169 of file string_constraint_generator.h.

◆ ns

const namespacet string_constraint_generatort::ns

Definition at line 139 of file string_constraint_generator.h.


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