#include <string_constraint_generator.h>
◆ string_constraint_generatort()
string_constraint_generatort::string_constraint_generatort |
( |
const namespacet & |
ns | ) |
|
|
explicit |
◆ add_axioms_for_function_application()
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_symbol | generator of fresh symbols |
expr | an 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()
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_symbol | generator of fresh symbols |
f | function application with argument refined_string str |
pool | pool of arrays representing strings |
- Returns
- integer expression
hash(str)
Definition at line 190 of file string_constraint_generator_comparison.cpp.
◆ add_axioms_for_intern()
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_symbol | generator of fresh symbols |
f | function application with one string argument |
- Returns
- a string expression
Definition at line 310 of file string_constraint_generator_comparison.cpp.
◆ associate_array_to_pointer()
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
-
f | a 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()
Associate an integer length to a char array.
This adds an axiom ensuring that arr.length
and length
are equal.
- Parameters
-
f | a 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()
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.
◆ array_pool
◆ constraints
◆ fresh_symbol
◆ hash_code_of_string
◆ intern_of_string
◆ message
const messaget string_constraint_generatort::message |
|
private |
◆ ns
The documentation for this class was generated from the following files: