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

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

expran expression containing a function application
expression corresponding to the result of the function application

Definition at line 369 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 ( const function_application_exprt f,
array_poolt pool 

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]) \)
    ffunction application with argument refined_string str
    poolpool of arrays representing strings
    integer expression hash(str)

Definition at line 189 of file string_constraint_generator_comparison.cpp.

◆ add_axioms_for_intern()

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

Add axioms corresponding to the String.intern java function.

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

Not tested.
never tested
ffunction application with one string argument
a string expression

Definition at line 307 of file string_constraint_generator_comparison.cpp.

◆ associate_array_to_pointer()

exprt string_constraint_generatort::associate_array_to_pointer ( const function_application_exprt f)

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.

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)

Associate an integer length to a char array.

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

fa function application with argument a character array arr and an integer length.
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.

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 134 of file string_constraint_generator.h.

◆ constraints

string_constraintst string_constraint_generatort::constraints

Definition at line 136 of file string_constraint_generator.h.

◆ fresh_symbol

symbol_generatort string_constraint_generatort::fresh_symbol

Definition at line 132 of file string_constraint_generator.h.

◆ hash_code_of_string

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

Definition at line 170 of file string_constraint_generator.h.

◆ intern_of_string

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

Definition at line 173 of file string_constraint_generator.h.

◆ message

const messaget string_constraint_generatort::message

Definition at line 166 of file string_constraint_generator.h.

◆ ns

const namespacet string_constraint_generatort::ns

Definition at line 138 of file string_constraint_generator.h.

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