cprover
|
#include <string_constraint_generator.h>
Classes | |
class | format_specifiert |
Public Member Functions | |
string_constraint_generatort (const namespacet &ns) | |
const std::vector< exprt > & | get_lemmas () const |
Axioms are of three kinds: universally quantified string constraint, not contains string constraints and simple formulas. More... | |
void | add_lemma (const exprt &) |
const std::vector< string_constraintt > & | get_constraints () const |
const std::vector< string_not_contains_constraintt > & | get_not_contains_constraints () const |
void | clear_constraints () |
Clear all constraints and lemmas. More... | |
const std::vector< symbol_exprt > & | get_boolean_symbols () const |
Boolean symbols for the results of some string functions. More... | |
const std::vector< symbol_exprt > & | get_index_symbols () const |
Symbols used in existential quantifications. More... | |
const std::set< array_string_exprt > & | get_created_strings () const |
Set of strings that have been created by the generator. More... | |
exprt | get_witness_of (const string_not_contains_constraintt &c, const exprt &univ_val) const |
exprt | 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. More... | |
symbol_exprt | fresh_univ_index (const irep_idt &prefix, const typet &type) |
generate an index symbol to be used as an universaly quantified variable More... | |
symbol_exprt | fresh_exist_index (const irep_idt &prefix, const typet &type) |
generate an index symbol which is existentially quantified More... | |
optionalt< exprt > | make_array_pointer_association (const function_application_exprt &expr) |
Associate array to pointer, and array to length. More... | |
const signedbv_typet | get_return_code_type () |
exprt | add_axioms_for_concat_char (const array_string_exprt &res, const array_string_exprt &s1, const exprt &c) |
Add axioms enforcing that res is the concatenation of s1 with character c . More... | |
exprt | 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 . More... | |
exprt | 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 index end_index'`. More... | |
exprt | add_axioms_for_insert (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &offset) |
Add axioms ensuring the result res corresponds to s1 where we inserted s2 at position offset . More... | |
exprt | add_axioms_for_string_of_int_with_radix (const array_string_exprt &res, const exprt &input_int, const exprt &radix, size_t max_size=0) |
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... | |
exprt | add_axioms_for_set_char (const array_string_exprt &res, const array_string_exprt &str, const exprt &position, const exprt &character) |
Add axioms ensuring that the result res is similar to input string str where the character at index pos is set to char . More... | |
exprt | add_axioms_for_to_lower_case (const array_string_exprt &res, const array_string_exprt &str) |
Add axioms ensuring res corresponds to str in which uppercase characters have been converted to lowercase. More... | |
exprt | add_axioms_for_to_upper_case (const array_string_exprt &res, const array_string_exprt &expr) |
Add axioms ensuring res corresponds to str in which lowercase characters of Basic Latin and Latin-1 supplement of unicode have been converted to uppercase. More... | |
Public Attributes | |
symbol_generatort | fresh_symbol |
array_poolt | array_pool |
std::map< string_not_contains_constraintt, symbol_exprt > | witness |
Private Member Functions | |
symbol_exprt | fresh_boolean (const irep_idt &prefix) |
generate a Boolean symbol which is existentially quantified More... | |
array_string_exprt | fresh_string (const typet &index_type, const typet &char_type) |
construct a string expression whose length and content are new variables More... | |
array_string_exprt | get_string_expr (const exprt &expr) |
casts an expression to a string expression, or fetches the actual string_exprt in the case of a symbol. More... | |
const array_string_exprt & | char_array_of_pointer (const exprt &pointer, const exprt &length) |
Adds creates a new array if it does not already exists. More... | |
exprt | axiom_for_is_positive_index (const exprt &x) |
expression true exactly when the index is positive More... | |
void | 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... | |
exprt | add_axioms_for_constrain_characters (const function_application_exprt &f) |
Add axioms to ensure all characters of a string belong to a given set. More... | |
exprt | add_axioms_for_char_at (const function_application_exprt &f) |
Character at a given position. More... | |
exprt | add_axioms_for_code_point_at (const function_application_exprt &f) |
add axioms corresponding to the String.codePointAt java function More... | |
exprt | add_axioms_for_code_point_before (const function_application_exprt &f) |
add axioms corresponding to the String.codePointBefore java function More... | |
exprt | add_axioms_for_contains (const function_application_exprt &f) |
Test whether a string contains another. More... | |
exprt | add_axioms_for_equals (const function_application_exprt &f) |
Equality of the content of two strings. More... | |
exprt | add_axioms_for_equals_ignore_case (const function_application_exprt &f) |
Equality of the content ignoring case of characters. More... | |
exprt | add_axioms_for_hash_code (const function_application_exprt &f) |
Value that is identical for strings with the same content. More... | |
exprt | 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. More... | |
exprt | 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. More... | |
exprt | add_axioms_for_is_prefix (const function_application_exprt &f, bool swap_arguments=false) |
Test if the target is a prefix of the string. More... | |
exprt | add_axioms_for_is_suffix (const function_application_exprt &f, bool swap_arguments=false) |
Test if the target is a suffix of the string. More... | |
exprt | add_axioms_for_length (const function_application_exprt &f) |
Length of a string. More... | |
exprt | add_axioms_for_empty_string (const function_application_exprt &f) |
Add axioms to say that the returned string expression is empty. More... | |
exprt | add_axioms_for_char_set (const function_application_exprt &f) |
Set a character to a specific value at an index of the string. More... | |
exprt | 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 More... | |
exprt | add_axioms_for_concat_char (const function_application_exprt &f) |
Add axioms enforcing that the string represented by the two first expressions is equal to the concatenation of the string argument and the character argument of the function application. More... | |
exprt | add_axioms_for_concat (const function_application_exprt &f) |
String concatenation. More... | |
exprt | add_axioms_for_concat_code_point (const function_application_exprt &f) |
Add axioms corresponding to the StringBuilder.appendCodePoint(I) function. More... | |
exprt | 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. More... | |
exprt | 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). More... | |
exprt | add_axioms_for_delete (const function_application_exprt &f) |
Remove a portion of a string. More... | |
exprt | add_axioms_for_delete_char_at (const function_application_exprt &expr) |
add axioms corresponding to the StringBuilder.deleteCharAt java function More... | |
exprt | add_axioms_for_format (const function_application_exprt &f) |
Formatted string using a format string and list of arguments. More... | |
exprt | add_axioms_for_format (const array_string_exprt &res, const std::string &s, const exprt::operandst &args) |
Parse s and add axioms ensuring the output corresponds to the output of String.format. More... | |
array_string_exprt | add_axioms_for_format_specifier (const format_specifiert &fs, const struct_exprt &arg, const typet &index_type, const typet &char_type) |
Parse s and add axioms ensuring the output corresponds to the output of String.format. More... | |
exprt | add_axioms_for_insert (const function_application_exprt &f) |
Insertion of a string in another at a specific index. More... | |
exprt | add_axioms_for_insert_int (const function_application_exprt &f) |
add axioms corresponding to the StringBuilder.insert(I) java function More... | |
exprt | add_axioms_for_insert_bool (const function_application_exprt &f) |
add axioms corresponding to the StringBuilder.insert(Z) java function More... | |
exprt | add_axioms_for_insert_char (const function_application_exprt &f) |
Add axioms corresponding to the StringBuilder.insert(C) java function. More... | |
exprt | add_axioms_for_insert_float (const function_application_exprt &f) |
Add axioms corresponding to the StringBuilder.insert(F) java function. More... | |
exprt | add_axioms_for_insert_double (const function_application_exprt &f) |
add axioms corresponding to the StringBuilder.insert(D) java function More... | |
exprt | 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. More... | |
exprt | add_axioms_from_literal (const function_application_exprt &f) |
String corresponding to an internal cprover string. More... | |
exprt | add_axioms_from_int (const function_application_exprt &f) |
Convert an integer to a string. More... | |
exprt | add_axioms_for_string_of_int (const array_string_exprt &res, const exprt &input_int, size_t max_size=0) |
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... | |
exprt | add_axioms_from_int_hex (const array_string_exprt &res, const exprt &i) |
exprt | add_axioms_from_int_hex (const function_application_exprt &f) |
Add axioms corresponding to the Integer.toHexString(I) java function. More... | |
exprt | add_axioms_from_long (const function_application_exprt &f) |
Add axioms corresponding to the String.valueOf(J) java function. More... | |
exprt | add_axioms_from_bool (const function_application_exprt &f) |
Add axioms corresponding to the String.valueOf(Z) java function. More... | |
exprt | add_axioms_from_bool (const array_string_exprt &res, const exprt &i) |
Add axioms stating that the returned string equals "true" when the Boolean expression is true and "false" when it is false. More... | |
exprt | add_axioms_from_char (const function_application_exprt &f) |
Conversion from char to string. More... | |
exprt | add_axioms_from_char (const array_string_exprt &res, const exprt &i) |
Add axiom stating that string res has length 1 and the character it contains equals c . More... | |
exprt | 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 . More... | |
exprt | 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 . More... | |
exprt | add_axioms_for_index_of (const function_application_exprt &f) |
Index of the first occurence of a target inside the string. More... | |
exprt | 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. More... | |
exprt | 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 . More... | |
exprt | add_axioms_for_last_index_of (const function_application_exprt &f) |
Index of the last occurence of a target inside the string. More... | |
exprt | add_axioms_for_string_of_float (const function_application_exprt &f) |
String representation of a float value. More... | |
exprt | 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 '. More... | |
exprt | add_axioms_for_fractional_part (const array_string_exprt &res, const exprt &i, size_t max_size) |
Add axioms for representing the fractional part of a floating point starting with a dot. More... | |
exprt | add_axioms_from_float_scientific_notation (const array_string_exprt &res, const exprt &f) |
Add axioms to write the float in scientific notation. More... | |
exprt | add_axioms_from_float_scientific_notation (const function_application_exprt &f) |
Representation of a float value in scientific notation. More... | |
exprt | add_axioms_from_double (const function_application_exprt &f) |
Add axioms corresponding to the String.valueOf(D) java function. More... | |
exprt | add_axioms_for_replace (const function_application_exprt &f) |
Replace a character by another in a string. More... | |
exprt | add_axioms_for_set_length (const function_application_exprt &f) |
Reduce or extend a string to have the given length. More... | |
exprt | 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')`. More... | |
exprt | add_axioms_for_substring (const function_application_exprt &f) |
Substring of a string between two indices. More... | |
exprt | add_axioms_for_to_lower_case (const function_application_exprt &f) |
Conversion of a string to lower case. More... | |
exprt | add_axioms_for_to_upper_case (const function_application_exprt &f) |
Conversion of a string to upper case. More... | |
exprt | add_axioms_for_trim (const function_application_exprt &f) |
Remove leading and trailing whitespaces. More... | |
exprt | 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 More... | |
exprt | add_axioms_for_char_literal (const function_application_exprt &f) |
add axioms stating that the returned value is equal to the argument More... | |
exprt | add_axioms_for_code_point_count (const function_application_exprt &f) |
Add axioms corresponding the String.codePointCount java function. More... | |
exprt | add_axioms_for_offset_by_code_point (const function_application_exprt &f) |
Add axioms corresponding the String.offsetByCodePointCount java function. More... | |
void | 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... | |
void | add_axioms_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... | |
exprt | add_axioms_for_parse_int (const function_application_exprt &f) |
Integer value represented by a string. More... | |
exprt | add_axioms_for_compare_to (const function_application_exprt &f) |
Lexicographic comparison of two strings. More... | |
symbol_exprt | add_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... | |
unsigned long | to_integer_or_default (const exprt &expr, unsigned long def) |
If the expression is a constant expression then we get the value of it as an unsigned long. More... | |
Static Private Member Functions | |
static constant_exprt | constant_char (int i, const typet &char_type) |
generate constant character expression with character type. More... | |
static exprt | int_of_hex_char (const exprt &chr) |
Returns the integer value represented by the character. More... | |
static exprt | is_high_surrogate (const exprt &chr) |
the output is true when the character is a high surrogate for UTF-16 encoding, see https://en.wikipedia.org/wiki/UTF-16 for more explenation about the encoding; this is true when the character is in the range 0xD800..0xDBFF More... | |
static exprt | is_low_surrogate (const exprt &chr) |
the output is true when the character is a low surrogate for UTF-16 encoding, see https://en.wikipedia.org/wiki/UTF-16 for more explenation about the encoding; this is true when the character is in the range 0xDC00..0xDFFF More... | |
static exprt | character_equals_ignore_case (exprt char1, exprt char2, exprt char_a, exprt char_A, exprt char_Z) |
Returns an expression which is true when the two given characters are equal when ignoring case for ASCII. More... | |
Private Attributes | |
std::set< array_string_exprt > | created_strings |
const messaget | message |
std::vector< exprt > | lemmas |
std::vector< string_constraintt > | constraints |
std::vector< string_not_contains_constraintt > | not_contains_constraints |
std::vector< symbol_exprt > | boolean_symbols |
std::vector< symbol_exprt > | index_symbols |
const namespacet | ns |
std::map< array_string_exprt, exprt > | hash_code_of_string |
std::map< array_string_exprt, symbol_exprt > | intern_of_string |
Definition at line 87 of file string_constraint_generator.h.
|
explicit |
Definition at line 31 of file string_constraint_generator_main.cpp.
|
private |
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] \).
f | function application with arguments string str and integer i |
char
Definition at line 600 of file string_constraint_generator_main.cpp.
References function_application_exprt::arguments(), fresh_symbol, get_string_expr(), lemmas, and PRECONDITION.
Referenced by add_axioms_for_function_application().
|
private |
add axioms stating that the returned value is equal to the argument
f | function application with one character argument |
Definition at line 565 of file string_constraint_generator_main.cpp.
References function_application_exprt::arguments(), CHECK_RETURN, from_integer(), string_constantt::get_value(), PRECONDITION, to_string_constant(), and UNIMPLEMENTED.
Referenced by add_axioms_for_function_application().
|
private |
Set a character to a specific value at an index of the string.
Add axioms ensuring that the result res
is similar to input string str
where the character at index pos
is set to char
. If pos
is out of bounds the string returned unchanged.
These axioms are:
1
when pos
is out of bounds and 0
otherwise f | function application with arguments integer |res| , character pointer &res[0] , refined_string str , integer pos , and character char |
Definition at line 398 of file string_constraint_generator_transformation.cpp.
References add_axioms_for_set_char(), function_application_exprt::arguments(), char_array_of_pointer(), get_string_expr(), and PRECONDITION.
|
private |
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.
input_int | the integer represented by str |
type | the type for input_int |
strict_formatting | if true, don't allow a leading plus, redundant zeros or upper case letters |
str | input string |
max_string_length | the maximum length str can have |
radix | the radix, with the same type as input_int |
radix_ul | the 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 404 of file string_constraint_generator_valueof.cpp.
References string_exprt< child_t >::axiom_for_has_length(), char_type(), conjunction(), constant_char(), array_string_exprt::content(), from_integer(), get_numeric_value_from_character(), lemmas, typet::subtype(), and exprt::type().
Referenced by add_axioms_for_parse_int(), and add_axioms_for_string_of_int_with_radix().
|
private |
add axioms for the conversion of an integer representing a java code point to a utf-16 string
res | array of characters corresponding to the result fo the function |
code_point | an expression representing a java code point |
Definition at line 20 of file string_constraint_generator_code_points.cpp.
References string_exprt< child_t >::axiom_for_has_length(), char_type(), array_string_exprt::content(), from_integer(), get_return_code_type(), irept::id(), lemmas, PRECONDITION, typet::subtype(), and exprt::type().
Referenced by add_axioms_for_concat_code_point().
|
private |
add axioms corresponding to the String.codePointAt java function
f | function application with arguments a string and an index |
Definition at line 119 of file string_constraint_generator_code_points.cpp.
References function_application_exprt::arguments(), fresh_symbol, from_integer(), get_string_expr(), irept::id(), is_high_surrogate(), is_low_surrogate(), lemmas, pair_value(), pos(), PRECONDITION, and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
add axioms corresponding to the String.codePointBefore java function
Definition at line 148 of file string_constraint_generator_code_points.cpp.
References function_application_exprt::arguments(), fresh_symbol, from_integer(), get_string_expr(), is_high_surrogate(), is_low_surrogate(), lemmas, array_string_exprt::length(), pair_value(), PRECONDITION, and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
Add axioms corresponding the String.codePointCount java function.
add axioms giving approximate bounds on the result of the String.codePointCount java function
f | function application with three arguments string str , integer begin and integer end . |
Definition at line 180 of file string_constraint_generator_code_points.cpp.
References function_application_exprt::arguments(), fresh_symbol, from_integer(), get_string_expr(), lemmas, minimum(), PRECONDITION, and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
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:
f | function application with arguments refined_string s1 and refined_string s2 |
res
Definition at line 220 of file string_constraint_generator_comparison.cpp.
References function_application_exprt::arguments(), constraints, fresh_exist_index(), fresh_symbol, fresh_univ_index(), from_integer(), get_string_expr(), index_type(), lemmas, PRECONDITION, exprt::type(), and zero_if_negative().
Referenced by add_axioms_for_function_application().
exprt 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
.
res | string_expression corresponding to the result |
s1 | the string expression to append to |
s2 | the string expression to append to the first one |
Definition at line 153 of file string_constraint_generator_concat.cpp.
References add_axioms_for_concat_substr(), and from_integer().
Referenced by add_axioms_for_concat(), add_axioms_for_concat_code_point(), add_axioms_for_delete(), add_axioms_for_format(), add_axioms_for_string_of_float(), add_axioms_from_float_scientific_notation(), and string_concatenation_builtin_functiont::add_constraints().
|
private |
String concatenation.
This primitive accepts 4 or 6 arguments. Add axioms enforcing that res
is the concatenation of s1
with the substring of s2
starting at index ‘start_index’and ending at index
end_index'`. (More...)
f | function application with arguments integer |res| , character pointer &res[0] , refined_string s1 , refined_string s2 , optional integer start_index , optional integer end_index |
Definition at line 173 of file string_constraint_generator_concat.cpp.
References add_axioms_for_concat(), add_axioms_for_concat_substr(), function_application_exprt::arguments(), char_array_of_pointer(), get_string_expr(), and PRECONDITION.
exprt string_constraint_generatort::add_axioms_for_concat_char | ( | const array_string_exprt & | res, |
const array_string_exprt & | s1, | ||
const exprt & | c | ||
) |
Add axioms enforcing that res
is the concatenation of s1
with character c
.
These axioms are :
res | string expression |
s1 | string expression |
c | character expression |
Definition at line 115 of file string_constraint_generator_concat.cpp.
References constraints, fresh_univ_index(), from_integer(), get_return_code_type(), index_type(), lemmas, array_string_exprt::length(), length_constraint_for_concat_char(), exprt::type(), and zero_if_negative().
Referenced by add_axioms_for_concat_char(), and string_concat_char_builtin_functiont::add_constraints().
|
private |
Add axioms enforcing that the string represented by the two first expressions is equal to the concatenation of the string argument and the character argument of the function application.
f | function application with a length, pointer, string and character argument. |
Definition at line 194 of file string_constraint_generator_concat.cpp.
References add_axioms_for_concat_char(), function_application_exprt::arguments(), char_array_of_pointer(), get_string_expr(), and PRECONDITION.
|
private |
Add axioms corresponding to the StringBuilder.appendCodePoint(I) function.
f | function application with two arguments: a string and a code point |
Definition at line 209 of file string_constraint_generator_concat.cpp.
References add_axioms_for_code_point(), add_axioms_for_concat(), function_application_exprt::arguments(), char_array_of_pointer(), char_type(), fresh_string(), get_string_expr(), index_type(), PRECONDITION, and typet::subtype().
Referenced by add_axioms_for_function_application().
exprt 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 index
end_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:
res | an array of characters expression |
s1 | an array of characters expression |
s2 | an array of characters expression |
start_index | integer expression |
end_index | integer expression |
0
Definition at line 37 of file string_constraint_generator_concat.cpp.
References constraints, fresh_univ_index(), from_integer(), get_return_code_type(), index_type(), lemmas, array_string_exprt::length(), length_constraint_for_concat_substr(), maximum(), minimum(), exprt::type(), and zero_if_negative().
Referenced by add_axioms_for_concat(), and string_concatenation_builtin_functiont::add_constraints().
|
private |
Add axioms ensuring that the provided string expression and constant are equal.
res | array of characters for the result |
sval | a string constant |
guard | condition under which the axiom should apply, true by default |
Definition at line 24 of file string_constraint_generator_constants.cpp.
References char_type(), array_string_exprt::content(), from_integer(), get_return_code_type(), id2string(), index_type(), lemmas, array_string_exprt::length(), typet::subtype(), exprt::type(), and widen().
Referenced by add_axioms_for_cprover_string(), add_axioms_for_format(), add_axioms_for_format_specifier(), and add_axioms_from_float_scientific_notation().
|
private |
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\).
f | a function application with arguments: integer |s| , character pointer &s[0] , string char_set_string , optional integers start and end |
Definition at line 342 of file string_constraint_generator_main.cpp.
References add_constraint_on_characters(), function_application_exprt::arguments(), dstringt::c_str(), char_array_of_pointer(), from_integer(), get_return_code_type(), constant_exprt::get_value(), array_string_exprt::length(), PRECONDITION, to_constant_expr(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
Test whether a string contains another.
Add axioms ensuring the returned value is true when the first string contains the second. These axioms are:
f | function application with arguments refined_string s0 refined_string s1 |
contains
Definition at line 212 of file string_constraint_generator_testing.cpp.
References function_application_exprt::arguments(), axiom_for_is_positive_index(), constraints, fresh_boolean(), fresh_exist_index(), fresh_univ_index(), from_integer(), get_string_expr(), irept::id(), index_type(), lemmas, not_contains_constraints, PRECONDITION, exprt::type(), and zero_if_negative().
Referenced by add_axioms_for_function_application().
|
private |
add axioms to say that the returned string expression is equal to the argument of the function application
f | function application with one argument, which is a string, or three arguments: string, integer offset and count |
Definition at line 528 of file string_constraint_generator_main.cpp.
References from_integer(), index_type(), array_string_exprt::length(), PRECONDITION, and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
Add axioms making the return value true if the given string is a correct number in the given radix.
str | string expression |
radix_as_char | the radix as an expression of the same type as the characters in str |
radix_ul | the radix, which should be between 2 and 36, or 0, in which case the return value will work for any radix |
max_size | maximum number of characters |
strict_formatting | if 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 319 of file string_constraint_generator_valueof.cpp.
References string_exprt< child_t >::axiom_for_has_length(), string_exprt< child_t >::axiom_for_length_ge(), string_exprt< child_t >::axiom_for_length_le(), char_type(), constant_char(), array_string_exprt::content(), from_integer(), index_type(), is_digit_with_radix(), lemmas, array_string_exprt::length(), typet::subtype(), and exprt::type().
Referenced by add_axioms_for_parse_int(), and add_axioms_for_string_of_int_with_radix().
|
private |
Convert an expression of type string_typet to a string_exprt.
res | string expression for the result |
arg | expression of type string typet |
guard | condition under which res should be equal to arg |
Definition at line 77 of file string_constraint_generator_constants.cpp.
References add_axioms_for_constant(), from_integer(), and get_return_code_type().
Referenced by add_axioms_from_literal().
|
private |
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).
res | array of characters expression |
str | array of characters expression |
start | integer expression |
end | integer expression |
Definition at line 563 of file string_constraint_generator_transformation.cpp.
References add_axioms_for_concat(), add_axioms_for_substring(), char_type(), array_string_exprt::content(), fresh_string(), from_integer(), index_type(), array_string_exprt::length(), PRECONDITION, typet::subtype(), and exprt::type().
Referenced by add_axioms_for_delete(), add_axioms_for_delete_char_at(), and add_axioms_for_function_application().
|
private |
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...)
f | function application with arguments integer |res| , character pointer &res[0] , refined_string str , integer start and integer end |
Definition at line 595 of file string_constraint_generator_transformation.cpp.
References add_axioms_for_delete(), function_application_exprt::arguments(), char_array_of_pointer(), get_string_expr(), and PRECONDITION.
|
private |
add axioms corresponding to the StringBuilder.deleteCharAt java function
f | function application with two arguments, the first is a string and the second is an index |
Definition at line 537 of file string_constraint_generator_transformation.cpp.
References add_axioms_for_delete(), function_application_exprt::arguments(), char_array_of_pointer(), from_integer(), get_string_expr(), and PRECONDITION.
Referenced by add_axioms_for_function_application().
|
private |
Add axioms to say that the returned string expression is empty.
f | function application with arguments integer length and character pointer ptr . |
Definition at line 61 of file string_constraint_generator_constants.cpp.
References function_application_exprt::arguments(), from_integer(), get_return_code_type(), lemmas, and PRECONDITION.
Referenced by add_axioms_for_function_application().
|
private |
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:
f | function application with arguments refined_string s1 and refined_string s2 |
eq
Definition at line 29 of file string_constraint_generator_comparison.cpp.
References function_application_exprt::arguments(), constraints, fresh_boolean(), fresh_exist_index(), fresh_univ_index(), from_integer(), get_string_expr(), irept::id(), index_type(), lemmas, PRECONDITION, exprt::type(), witness, and zero_if_negative().
Referenced by add_axioms_for_function_application().
|
private |
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:
f | function application with arguments refined_string s1 and refined_string s2 |
eq
Definition at line 121 of file string_constraint_generator_comparison.cpp.
References function_application_exprt::arguments(), char_type(), character_equals_ignore_case(), constant_char(), constraints, fresh_boolean(), fresh_exist_index(), fresh_univ_index(), from_integer(), get_string_expr(), irept::id(), index_type(), lemmas, PRECONDITION, typet::subtype(), exprt::type(), witness, and zero_if_negative().
Referenced by add_axioms_for_function_application().
|
private |
Formatted string using a format string and list of arguments.
Add axioms to specify the Java String.format function.
f | a function application |
Definition at line 460 of file string_constraint_generator_format.cpp.
References function_application_exprt::arguments(), char_array_of_pointer(), messaget::eom(), from_integer(), get_string_expr(), message, PRECONDITION, to_array_expr(), to_constant_expr(), to_unsigned_integer(), exprt::type(), utf16_constant_array_to_java(), and messaget::warning().
Referenced by add_axioms_for_function_application().
|
private |
Parse s
and add axioms ensuring the output corresponds to the output of String.format.
res | string expression for the result of the format function |
s | a format string |
args | a vector of arguments |
Definition at line 349 of file string_constraint_generator_format.cpp.
References add_axioms_for_concat(), add_axioms_for_constant(), add_axioms_for_format_specifier(), add_axioms_for_substring(), char_type(), array_string_exprt::content(), string_constraint_generatort::format_specifiert::conversion, fresh_string(), from_integer(), get_return_code_type(), string_constraint_generatort::format_specifiert::index, index_type(), INVARIANT, lemmas, array_string_exprt::length(), string_constraint_generatort::format_specifiert::LINE_SEPARATOR, parse_format_string(), string_constraint_generatort::format_specifiert::PERCENT_SIGN, typet::subtype(), to_struct_expr(), and exprt::type().
|
private |
Parse s
and add axioms ensuring the output corresponds to the output of String.format.
Assumes the argument is a structured expression which contains the fields: string expr, int, float, char, boolean, hashcode, date_time. The correct component will be fetched depending on the format specifier.
fs | a format specifier |
arg | a struct containing the possible value of the argument to format |
index_type | type for indexes in strings |
char_type | type of characters |
Definition at line 260 of file string_constraint_generator_format.cpp.
References add_axioms_for_constant(), add_axioms_for_string_of_float(), add_axioms_for_string_of_int(), add_axioms_for_to_upper_case(), add_axioms_from_bool(), add_axioms_from_char(), add_axioms_from_float_scientific_notation(), add_axioms_from_int_hex(), string_constraint_generatort::format_specifiert::BOOLEAN, string_constraint_generatort::format_specifiert::BOOLEAN_UPPER, char_type(), string_constraint_generatort::format_specifiert::CHARACTER, string_constraint_generatort::format_specifiert::CHARACTER_UPPER, string_constraint_generatort::format_specifiert::conversion, string_constraint_generatort::format_specifiert::DATE_TIME, string_constraint_generatort::format_specifiert::DATE_TIME_UPPER, string_constraint_generatort::format_specifiert::DECIMAL_FLOAT, string_constraint_generatort::format_specifiert::DECIMAL_INTEGER, messaget::eom(), messaget::error(), fresh_string(), string_constraint_generatort::format_specifiert::GENERAL, string_constraint_generatort::format_specifiert::GENERAL_UPPER, get_component_in_struct(), get_string_expr(), string_constraint_generatort::format_specifiert::HASHCODE, string_constraint_generatort::format_specifiert::HASHCODE_UPPER, string_constraint_generatort::format_specifiert::HEXADECIMAL_FLOAT, string_constraint_generatort::format_specifiert::HEXADECIMAL_FLOAT_UPPER, string_constraint_generatort::format_specifiert::HEXADECIMAL_INTEGER, index_type(), INVARIANT, string_constraint_generatort::format_specifiert::LINE_SEPARATOR, message, string_constraint_generatort::format_specifiert::OCTAL_INTEGER, string_constraint_generatort::format_specifiert::PERCENT_SIGN, string_constraint_generatort::format_specifiert::SCIENTIFIC, string_constraint_generatort::format_specifiert::SCIENTIFIC_UPPER, string_constraint_generatort::format_specifiert::STRING, string_constraint_generatort::format_specifiert::STRING_UPPER, and messaget::warning().
Referenced by add_axioms_for_format().
|
private |
Add axioms for representing the fractional part of a floating point starting with a dot.
res | string expression for the result |
int_expr | an integer expression |
max_size | a maximal size for the string, this includes the potential minus sign and therefore should be greater than 2 |
Definition at line 229 of file string_constraint_generator_float.cpp.
References string_exprt< child_t >::axiom_for_length_gt(), string_exprt< child_t >::axiom_for_length_le(), char_type(), conjunction(), constant_char(), array_string_exprt::content(), from_integer(), irept::id(), index_type(), is_number(), lemmas, array_string_exprt::length(), PRECONDITION, typet::subtype(), and exprt::type().
Referenced by add_axioms_for_string_of_float(), and add_axioms_from_float_scientific_notation().
exprt 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.
Definition at line 411 of file string_constraint_generator_main.cpp.
References add_axioms_for_char_at(), add_axioms_for_char_literal(), add_axioms_for_code_point_at(), add_axioms_for_code_point_before(), add_axioms_for_code_point_count(), add_axioms_for_compare_to(), add_axioms_for_concat_code_point(), add_axioms_for_constrain_characters(), add_axioms_for_contains(), add_axioms_for_copy(), add_axioms_for_delete(), add_axioms_for_delete_char_at(), add_axioms_for_empty_string(), add_axioms_for_equals(), add_axioms_for_equals_ignore_case(), add_axioms_for_format(), add_axioms_for_hash_code(), add_axioms_for_index_of(), add_axioms_for_insert(), add_axioms_for_insert_bool(), add_axioms_for_insert_char(), add_axioms_for_insert_double(), add_axioms_for_insert_float(), add_axioms_for_insert_int(), add_axioms_for_intern(), add_axioms_for_is_empty(), add_axioms_for_is_prefix(), add_axioms_for_is_suffix(), add_axioms_for_last_index_of(), add_axioms_for_length(), add_axioms_for_offset_by_code_point(), add_axioms_for_parse_int(), add_axioms_for_replace(), add_axioms_for_set_length(), add_axioms_for_string_of_float(), add_axioms_for_substring(), add_axioms_for_trim(), add_axioms_from_bool(), add_axioms_from_char(), add_axioms_from_double(), add_axioms_from_float_scientific_notation(), add_axioms_from_int_hex(), add_axioms_from_literal(), add_axioms_from_long(), DATA_INVARIANT, get_function_name(), id2string(), and string_refinement_invariantt.
Referenced by string_builtin_function_with_no_evalt::add_constraints().
|
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:
f | function application with argument refined_string str |
hash(str)
Definition at line 174 of file string_constraint_generator_comparison.cpp.
References function_application_exprt::arguments(), axiom_for_is_positive_index(), fresh_exist_index(), fresh_symbol, get_string_expr(), hash_code_of_string, index_type(), lemmas, PRECONDITION, and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
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:
str | an array of characters expression |
c | a character expression |
from_index | an integer expression |
index
Definition at line 37 of file string_constraint_generator_indexof.cpp.
References constraints, fresh_boolean(), fresh_exist_index(), fresh_univ_index(), from_integer(), index_type(), lemmas, array_string_exprt::length(), exprt::type(), and zero_if_negative().
Referenced by add_axioms_for_function_application().
|
private |
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...)
f | function application with arguments refined_string haystack , refined_string or character needle , and optional integer from_index with default value 0 |
Definition at line 281 of file string_constraint_generator_indexof.cpp.
References add_axioms_for_index_of(), add_axioms_for_index_of_string(), function_application_exprt::arguments(), char_type(), from_integer(), get_string_expr(), irept::id(), index_type(), INVARIANT, is_refined_string_type(), PRECONDITION, string_refinement_invariantt, typet::subtype(), and exprt::type().
Referenced by add_axioms_for_index_of().
|
private |
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:
haystack | an array of character expression |
needle | an array of character expression |
from_index | an integer expression |
index
representing the first index of needle
in haystack
Definition at line 107 of file string_constraint_generator_indexof.cpp.
References constraints, fresh_boolean(), fresh_exist_index(), fresh_univ_index(), from_integer(), index_type(), lemmas, array_string_exprt::length(), not_contains_constraints, exprt::type(), and zero_if_negative().
Referenced by add_axioms_for_index_of().
exprt 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 ensuring the result res
corresponds to s1
where we inserted s2
at position offset
.
We write offset' for max(0, min(res.length, offset))
. These axioms are:
res | array of characters expression |
s1 | array of characters expression |
s2 | array of characters expression |
offset | integer expression |
Definition at line 32 of file string_constraint_generator_insert.cpp.
References constraints, fresh_symbol, from_integer(), get_return_code_type(), index_type(), lemmas, length_constraint_for_insert(), maximum(), minimum(), PRECONDITION, exprt::type(), and zero_if_negative().
Referenced by add_axioms_for_function_application(), add_axioms_for_insert(), add_axioms_for_insert_char(), and string_insertion_builtin_functiont::add_constraints().
|
private |
Insertion of a string in another at a specific index.
Add axioms ensuring the result res
corresponds to s1
where we inserted s2
at position offset
. (More...)
If start
and end
arguments are given then substring(s2, start, end)
is considered instead of s2
.
f | function application with arguments integer |res| , character pointer &res[0] , refined_string s1 , refined_strings2 , integer offset , optional integer start and optional integer end |
Definition at line 101 of file string_constraint_generator_insert.cpp.
References add_axioms_for_insert(), add_axioms_for_substring(), function_application_exprt::arguments(), char_array_of_pointer(), char_type(), fresh_string(), from_integer(), get_string_expr(), index_type(), PRECONDITION, typet::subtype(), and exprt::type().
|
private |
add axioms corresponding to the StringBuilder.insert(Z) java function
f | function application with three arguments: a string, an integer offset, and a Boolean |
Definition at line 157 of file string_constraint_generator_insert.cpp.
References char_type(), index_type(), PRECONDITION, and typet::subtype().
Referenced by add_axioms_for_function_application().
|
private |
Add axioms corresponding to the StringBuilder.insert(C) java function.
f | function application with three arguments: a string, an integer offset, and a character |
Definition at line 177 of file string_constraint_generator_insert.cpp.
References add_axioms_for_insert(), add_axioms_from_char(), function_application_exprt::arguments(), char_array_of_pointer(), char_type(), fresh_string(), get_string_expr(), index_type(), PRECONDITION, and typet::subtype().
Referenced by add_axioms_for_function_application().
|
private |
add axioms corresponding to the StringBuilder.insert(D) java function
f | function application with three arguments: a string, an integer offset, and a double |
Definition at line 198 of file string_constraint_generator_insert.cpp.
References char_type(), index_type(), PRECONDITION, and typet::subtype().
Referenced by add_axioms_for_function_application().
|
private |
Add axioms corresponding to the StringBuilder.insert(F) java function.
f | function application with three arguments: a string, an integer offset, and a float |
Definition at line 220 of file string_constraint_generator_insert.cpp.
Referenced by add_axioms_for_function_application().
|
private |
add axioms corresponding to the StringBuilder.insert(I) java function
f | function application with three arguments: a string, an integer offset, and an integer |
Definition at line 136 of file string_constraint_generator_insert.cpp.
References char_type(), index_type(), PRECONDITION, and typet::subtype().
Referenced by add_axioms_for_function_application().
|
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.
f | function application with one string argument |
Definition at line 284 of file string_constraint_generator_comparison.cpp.
References disjunction(), index_type(), and PRECONDITION.
Referenced by add_axioms_for_function_application().
|
private |
Add axioms stating that the returned value is true exactly when the argument string is empty.
string_length(s)==0
instead f | function application with a string argument |
Definition at line 114 of file string_constraint_generator_testing.cpp.
References string_exprt< child_t >::axiom_for_has_length(), irept::id(), is_empty(), and PRECONDITION.
Referenced by add_axioms_for_function_application().
|
private |
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:
where offset_within_bounds is: offset >= 0 && offset <= |str| && |str| - offset >= |prefix|
prefix | an array of characters |
str | an array of characters |
offset | an integer |
isprefix
Definition at line 36 of file string_constraint_generator_testing.cpp.
References axiom_for_is_positive_index(), string_exprt< child_t >::axiom_for_length_ge(), string_exprt< child_t >::axiom_for_length_gt(), constraints, fresh_boolean(), fresh_exist_index(), fresh_univ_index(), from_integer(), index_type(), lemmas, array_string_exprt::length(), maximum(), exprt::type(), and witness.
Referenced by add_axioms_for_function_application(), and add_axioms_for_is_prefix().
|
private |
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)
f | a function application with arguments refined_string s0 , refined string s1 and optional integer argument offset whose default value is 0 |
swap_arguments | a Boolean telling whether the prefix is the second argument or the first argument |
isprefix
Definition at line 93 of file string_constraint_generator_testing.cpp.
References add_axioms_for_is_prefix(), function_application_exprt::arguments(), from_integer(), get_string_expr(), irept::id(), PRECONDITION, and exprt::type().
|
private |
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:
f | a function application with arguments refined_string s0 and refined_string s1 |
swap_arguments | boolean flag telling whether the suffix is the second argument or the first argument |
issuffix
Definition at line 151 of file string_constraint_generator_testing.cpp.
References from_integer(), irept::id(), index_type(), PRECONDITION, and zero_if_negative().
Referenced by add_axioms_for_function_application().
|
private |
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 :
str | an array of characters expression |
c | a character expression |
from_index | an 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 333 of file string_constraint_generator_indexof.cpp.
References constraints, fresh_boolean(), fresh_exist_index(), fresh_univ_index(), from_integer(), index_type(), lemmas, array_string_exprt::length(), exprt::type(), and zero_if_negative().
Referenced by add_axioms_for_function_application(), and add_axioms_for_last_index_of().
|
private |
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...)
f | function application with arguments refined_string haystack , refined_string or character needle , and optional integer from_index with default value |haystack|-1 |
Definition at line 398 of file string_constraint_generator_indexof.cpp.
References add_axioms_for_last_index_of(), add_axioms_for_last_index_of_string(), function_application_exprt::arguments(), char_type(), get_string_expr(), irept::id(), index_type(), PRECONDITION, typet::subtype(), and exprt::type().
|
private |
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:
haystack | an array of characters expression |
needle | an array of characters expression |
from_index | 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 199 of file string_constraint_generator_indexof.cpp.
References constraints, fresh_boolean(), fresh_exist_index(), fresh_univ_index(), from_integer(), index_type(), lemmas, array_string_exprt::length(), not_contains_constraints, exprt::type(), and zero_if_negative().
Referenced by add_axioms_for_last_index_of().
|
private |
Length of a string.
Returns the length of the string argument of the given function application
f | function application with argument string str |
|str|
Definition at line 546 of file string_constraint_generator_main.cpp.
References function_application_exprt::arguments(), get_string_expr(), array_string_exprt::length(), and PRECONDITION.
Referenced by add_axioms_for_function_application().
|
private |
Add axioms corresponding the String.offsetByCodePointCount java function.
add axioms giving approximate bounds on the result of the String.offsetByCodePointCount java function.
We approximate the result by saying the result is between index + offset and index + 2 * offset
f | function application with arguments string str , integer index and integer offset . |
Definition at line 203 of file string_constraint_generator_code_points.cpp.
References function_application_exprt::arguments(), fresh_symbol, lemmas, maximum(), minimum(), PRECONDITION, and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
Integer value represented by a string.
Add axioms ensuring the value of the returned integer corresponds to the value represented by str
f | a function application with arguments refined_string str and an optional integer for the radix |
str
Definition at line 491 of file string_constraint_generator_valueof.cpp.
References add_axioms_for_characters_in_integer_string(), add_axioms_for_correct_number_format(), function_application_exprt::arguments(), char_type(), fresh_symbol, from_integer(), get_string_expr(), max_printed_string_length(), PRECONDITION, typet::subtype(), to_integer_or_default(), and exprt::type().
Referenced by add_axioms_for_function_application().
|
private |
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:
f | function application with arguments integer |res| , character pointer &res[0] , refined_string str , character old_char and character new_char |
Definition at line 500 of file string_constraint_generator_transformation.cpp.
References function_application_exprt::arguments(), char_array_of_pointer(), constraints, fresh_univ_index(), from_integer(), get_string_expr(), lemmas, PRECONDITION, to_char_pair(), exprt::type(), and zero_if_negative().
Referenced by add_axioms_for_function_application().
exprt string_constraint_generatort::add_axioms_for_set_char | ( | const array_string_exprt & | res, |
const array_string_exprt & | str, | ||
const exprt & | position, | ||
const exprt & | character | ||
) |
Add axioms ensuring that the result res
is similar to input string str
where the character at index pos
is set to char
.
If pos
is out of bounds the string returned unchanged.
These axioms are:
1
when pos
is out of bounds and 0
otherwise Definition at line 421 of file string_constraint_generator_transformation.cpp.
References constraints, fresh_univ_index(), from_integer(), get_return_code_type(), lemmas, array_string_exprt::length(), minimum(), exprt::type(), and zero_if_negative().
Referenced by add_axioms_for_char_set(), and string_set_char_builtin_functiont::add_constraints().
|
private |
Reduce or extend a string to have the given length.
Add axioms ensuring the returned string expression res
has length k
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
.
These axioms are:
f | function application with arguments integer |res| , character pointer &res[0] , refined_string s1 , integer k |
0
Definition at line 35 of file string_constraint_generator_transformation.cpp.
References function_application_exprt::arguments(), char_array_of_pointer(), char_type(), constant_char(), constraints, fresh_univ_index(), from_integer(), get_string_expr(), index_type(), lemmas, minimum(), PRECONDITION, typet::subtype(), and zero_if_negative().
Referenced by add_axioms_for_function_application().
|
private |
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
f | function application with one float argument |
Definition at line 155 of file string_constraint_generator_float.cpp.
References function_application_exprt::arguments(), char_array_of_pointer(), and PRECONDITION.
Referenced by add_axioms_for_format_specifier(), add_axioms_for_function_application(), and add_axioms_from_double().
|
private |
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.
res | string expression corresponding to the result |
f | expression representing a float |
Definition at line 185 of file string_constraint_generator_float.cpp.
References add_axioms_for_concat(), add_axioms_for_fractional_part(), add_axioms_for_string_of_int(), char_type(), constant_float(), array_string_exprt::content(), floatbv_mult(), fresh_string(), from_integer(), index_type(), array_string_exprt::length(), round_expr_to_zero(), typet::subtype(), to_floatbv_type(), and exprt::type().
|
private |
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.
res | string expression for the result |
input_int | a signed integer expression |
max_size | a maximal size for the string representation (default 0, which is interpreted to mean "as large as is needed for this type") |
Definition at line 127 of file string_constraint_generator_valueof.cpp.
References add_axioms_for_string_of_int_with_radix(), from_integer(), and exprt::type().
Referenced by add_axioms_for_format_specifier(), add_axioms_for_string_of_float(), add_axioms_from_float_scientific_notation(), and add_axioms_from_int().
exprt 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 = 0 |
||
) |
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.
res | string expression for the result |
input_int | a signed integer expression |
radix | the radix to use |
max_size | a maximal size for the string representation (default 0, which is interpreted to mean "as large as is needed for this type") |
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 146 of file string_constraint_generator_valueof.cpp.
References add_axioms_for_characters_in_integer_string(), add_axioms_for_correct_number_format(), char_type(), CHECK_RETURN, array_string_exprt::content(), from_integer(), irept::id(), max_printed_string_length(), PRECONDITION, typet::subtype(), to_integer_or_default(), and exprt::type().
Referenced by add_axioms_for_string_of_int(), add_axioms_from_int(), and string_of_int_builtin_functiont::add_constraints().
|
private |
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:
res | array of characters expression |
str | array of characters expression |
start | integer expression |
end | integer expression |
Definition at line 116 of file string_constraint_generator_transformation.cpp.
References constraints, fresh_univ_index(), from_integer(), index_type(), lemmas, array_string_exprt::length(), maximum(), minimum(), PRECONDITION, exprt::type(), and zero_if_negative().
Referenced by add_axioms_for_delete(), add_axioms_for_format(), add_axioms_for_function_application(), add_axioms_for_insert(), and add_axioms_for_substring().
|
private |
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...)
f | function application with arguments integer |res| , character pointer &res[0] , refined_string str , integer start , optional integer end with default value |str| . |
Definition at line 90 of file string_constraint_generator_transformation.cpp.
References add_axioms_for_substring(), function_application_exprt::arguments(), char_array_of_pointer(), get_string_expr(), and PRECONDITION.
exprt string_constraint_generatort::add_axioms_for_to_lower_case | ( | const array_string_exprt & | res, |
const array_string_exprt & | str | ||
) |
Add axioms ensuring res
corresponds to str
in which uppercase characters have been converted to lowercase.
These axioms are:
Where diff
is the difference between lower case and upper case characters: ‘diff = 'a’-'A' = 0x20and
is_upper_case` is true for the upper case characters of Basic Latin and Latin-1 supplement of unicode.
Definition at line 300 of file string_constraint_generator_transformation.cpp.
References char_type(), constraints, fresh_univ_index(), from_integer(), get_return_code_type(), index_type(), is_upper_case(), lemmas, array_string_exprt::length(), typet::subtype(), exprt::type(), and zero_if_negative().
Referenced by add_axioms_for_to_lower_case(), and string_to_lower_case_builtin_functiont::add_constraints().
|
private |
Conversion of a string to lower case.
f | function application with arguments integer |res| , character pointer &res[0] , refined_string str |
0
when there is an exception to signal Definition at line 239 of file string_constraint_generator_transformation.cpp.
References add_axioms_for_to_lower_case(), function_application_exprt::arguments(), char_array_of_pointer(), get_string_expr(), and PRECONDITION.
exprt string_constraint_generatort::add_axioms_for_to_upper_case | ( | const array_string_exprt & | res, |
const array_string_exprt & | str | ||
) |
Add axioms ensuring res
corresponds to str
in which lowercase characters of Basic Latin and Latin-1 supplement of unicode have been converted to uppercase.
These axioms are:
res | array of characters expression |
str | array of characters expression |
0
when there is an exception to signal Definition at line 346 of file string_constraint_generator_transformation.cpp.
References char_type(), constant_char(), constraints, array_string_exprt::content(), fresh_univ_index(), from_integer(), get_return_code_type(), index_type(), is_lower_case(), lemmas, array_string_exprt::length(), typet::subtype(), exprt::type(), and zero_if_negative().
Referenced by add_axioms_for_format_specifier(), add_axioms_for_to_upper_case(), and string_to_upper_case_builtin_functiont::add_constraints().
|
private |
Conversion of a string to upper case.
Add axioms ensuring res
corresponds to str
in which lowercase characters of Basic Latin and Latin-1 supplement of unicode have been converted to uppercase. (More...)
f | function application with arguments integer |res| , character pointer &res[0] , refined_string str |
0
when there is an exception to signal Definition at line 383 of file string_constraint_generator_transformation.cpp.
References add_axioms_for_to_upper_case(), function_application_exprt::arguments(), char_array_of_pointer(), get_string_expr(), and PRECONDITION.
|
private |
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:
idx
represents the index of the first non-space character.f | function application with arguments integer |res| , character pointer &res[0] , refined_string str . |
Definition at line 170 of file string_constraint_generator_transformation.cpp.
References function_application_exprt::arguments(), char_array_of_pointer(), char_type(), constraints, fresh_exist_index(), fresh_univ_index(), from_integer(), get_string_expr(), index_type(), lemmas, PRECONDITION, typet::subtype(), exprt::type(), and zero_if_negative().
Referenced by add_axioms_for_function_application().
|
private |
Add axioms corresponding to the String.valueOf(Z) java function.
f | function application with a Boolean argument |
Definition at line 63 of file string_constraint_generator_valueof.cpp.
References PRECONDITION.
Referenced by add_axioms_for_format_specifier(), and add_axioms_for_function_application().
|
private |
Add axioms stating that the returned string equals "true" when the Boolean expression is true and "false" when it is false.
res | string expression for the result |
b | Boolean expression |
Definition at line 79 of file string_constraint_generator_valueof.cpp.
References char_type(), from_integer(), irept::id(), PRECONDITION, and typet::subtype().
|
private |
Conversion from char to string.
Add axiom stating that string res
has length 1 and the character it contains equals c
. (More...)
f | function application with arguments integer |res| , character pointer &res[0] and character c |
Definition at line 284 of file string_constraint_generator_valueof.cpp.
References function_application_exprt::arguments(), char_array_of_pointer(), and PRECONDITION.
Referenced by add_axioms_for_format_specifier(), add_axioms_for_function_application(), and add_axioms_for_insert_char().
|
private |
Add axiom stating that string res
has length 1 and the character it contains equals c
.
This axiom is: \( |{\tt res}| = 1 \land {\tt res}[0] = {\tt c} \).
res | array of characters expression |
c | character expression |
Definition at line 300 of file string_constraint_generator_valueof.cpp.
References string_exprt< child_t >::axiom_for_has_length(), from_integer(), get_return_code_type(), and lemmas.
|
private |
Add axioms corresponding to the String.valueOf(D) java function.
f | function application with one double argument |
Definition at line 167 of file string_constraint_generator_float.cpp.
References add_axioms_for_string_of_float().
Referenced by add_axioms_for_function_application().
|
private |
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))\)
res | string expression representing the float in scientific notation |
f | a float expression, which is positive |
Definition at line 315 of file string_constraint_generator_float.cpp.
References add_axioms_for_concat(), add_axioms_for_constant(), add_axioms_for_fractional_part(), add_axioms_for_string_of_int(), char_type(), constant_float(), array_string_exprt::content(), estimate_decimal_exponent(), float_type(), floatbv_mult(), floatbv_of_int_expr(), fresh_string(), from_integer(), get_exponent(), get_significand(), index_type(), array_string_exprt::length(), round_expr_to_zero(), ieee_floatt::ROUND_TO_ZERO, ieee_float_spect::single_precision(), typet::subtype(), ieee_float_spect::to_type(), and exprt::type().
Referenced by add_axioms_for_format_specifier(), add_axioms_for_function_application(), and add_axioms_from_float_scientific_notation().
|
private |
Representation of a float value in scientific notation.
Add axioms corresponding to the scientific representation of floating point values
f | a function application expression |
Definition at line 482 of file string_constraint_generator_float.cpp.
References add_axioms_from_float_scientific_notation(), function_application_exprt::arguments(), char_array_of_pointer(), and PRECONDITION.
|
private |
Convert an integer to a string.
Add axioms corresponding to the String.valueOf(I) java function.
f | function application with one integer argument |
Definition at line 27 of file string_constraint_generator_valueof.cpp.
References add_axioms_for_string_of_int(), add_axioms_for_string_of_int_with_radix(), function_application_exprt::arguments(), char_array_of_pointer(), and PRECONDITION.
|
private |
|
private |
Add axioms corresponding to the Integer.toHexString(I) java function.
f | function application with an integer argument |
Definition at line 265 of file string_constraint_generator_valueof.cpp.
References add_axioms_from_int_hex(), function_application_exprt::arguments(), char_array_of_pointer(), and PRECONDITION.
|
private |
String corresponding to an internal cprover string.
Add axioms ensuring that the returned string expression is equal to the string literal.
f | function application with an argument which is a string literal that is a constant with a string value. |
Definition at line 111 of file string_constraint_generator_constants.cpp.
References add_axioms_for_cprover_string(), function_application_exprt::arguments(), char_array_of_pointer(), and PRECONDITION.
Referenced by add_axioms_for_function_application().
|
private |
Add axioms corresponding to the String.valueOf(J) java function.
f | function application with one long argument |
Definition at line 45 of file string_constraint_generator_valueof.cpp.
References PRECONDITION.
Referenced by add_axioms_for_function_application().
|
private |
Add constraint on characters of a string.
This constraint is \( \forall i \in [start, end), low\_char \le s[i] \le high\_char \)
s | a string expression |
start | index of the first character to constrain |
end | index at which we stop adding constraints |
char_set | a 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 . |
Definition at line 309 of file string_constraint_generator_main.cpp.
References constraints, fresh_univ_index(), from_integer(), array_string_exprt::length(), PRECONDITION, exprt::type(), and zero_if_negative().
Referenced by add_axioms_for_constrain_characters().
void string_constraint_generatort::add_lemma | ( | const exprt & | expr | ) |
Definition at line 41 of file string_constraint_generator_main.cpp.
References lemmas.
Referenced by string_dependenciest::add_constraints().
|
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
.
f | a function application with argument a character array arr and a character pointer ptr . |
Definition at line 244 of file string_constraint_generator_main.cpp.
References function_application_exprt::arguments(), array_pool, created_strings, from_integer(), array_poolt::insert(), PRECONDITION, to_array_string_expr(), to_index_expr(), and exprt::type().
Referenced by make_array_pointer_association().
|
private |
Associate an integer length to a char array.
This adds an axiom ensuring that arr.length
and length
are equal.
f | a function application with argument a character array arr and a integer length . |
Definition at line 266 of file string_constraint_generator_main.cpp.
References function_application_exprt::arguments(), array_pool, from_integer(), array_poolt::get_length(), lemmas, PRECONDITION, to_array_string_expr(), and exprt::type().
Referenced by make_array_pointer_association().
expression true exactly when the index is positive
x | an index expression |
Definition at line 557 of file string_constraint_generator_main.cpp.
References from_integer(), and exprt::type().
Referenced by add_axioms_for_contains(), add_axioms_for_hash_code(), and add_axioms_for_is_prefix().
|
private |
Adds creates a new array if it does not already exists.
Definition at line 369 of file string_constraint_generator_main.cpp.
References array_pool, created_strings, and array_poolt::find().
Referenced by add_axioms_for_char_set(), add_axioms_for_concat(), add_axioms_for_concat_char(), add_axioms_for_concat_code_point(), add_axioms_for_constrain_characters(), add_axioms_for_delete(), add_axioms_for_delete_char_at(), add_axioms_for_format(), add_axioms_for_insert(), add_axioms_for_insert_char(), add_axioms_for_replace(), add_axioms_for_set_length(), add_axioms_for_string_of_float(), add_axioms_for_substring(), add_axioms_for_to_lower_case(), add_axioms_for_to_upper_case(), add_axioms_for_trim(), add_axioms_from_char(), add_axioms_from_float_scientific_notation(), add_axioms_from_int(), add_axioms_from_int_hex(), add_axioms_from_literal(), and get_string_expr().
|
staticprivate |
Returns an expression which is true when the two given characters are equal when ignoring case for ASCII.
char1 | character expression |
char2 | character expression |
char_a | constant character 'a' |
char_A | constant character 'A' |
char_Z | constant character 'Z' |
Definition at line 82 of file string_constraint_generator_comparison.cpp.
Referenced by add_axioms_for_equals_ignore_case().
void string_constraint_generatort::clear_constraints | ( | ) |
Clear all constraints and lemmas.
Definition at line 290 of file string_constraint_generator_main.cpp.
References constraints, lemmas, and not_contains_constraints.
Referenced by string_refinementt::dec_solve().
|
staticprivate |
generate constant character expression with character type.
Definition at line 82 of file string_constraint_generator_main.cpp.
References char_type(), and from_integer().
Referenced by add_axioms_for_characters_in_integer_string(), add_axioms_for_correct_number_format(), add_axioms_for_equals_ignore_case(), add_axioms_for_fractional_part(), add_axioms_for_set_length(), add_axioms_for_to_upper_case(), int_of_hex_char(), is_high_surrogate(), and is_low_surrogate().
|
private |
generate a Boolean symbol which is existentially quantified
Definition at line 124 of file string_constraint_generator_main.cpp.
References boolean_symbols, and fresh_symbol.
Referenced by add_axioms_for_contains(), add_axioms_for_equals(), add_axioms_for_equals_ignore_case(), add_axioms_for_index_of(), add_axioms_for_index_of_string(), add_axioms_for_is_prefix(), add_axioms_for_last_index_of(), and add_axioms_for_last_index_of_string().
symbol_exprt string_constraint_generatort::fresh_exist_index | ( | const irep_idt & | prefix, |
const typet & | type | ||
) |
generate an index symbol which is existentially quantified
Definition at line 113 of file string_constraint_generator_main.cpp.
References fresh_symbol, and index_symbols.
Referenced by add_axioms_for_compare_to(), add_axioms_for_contains(), add_axioms_for_equals(), add_axioms_for_equals_ignore_case(), add_axioms_for_hash_code(), add_axioms_for_index_of(), add_axioms_for_index_of_string(), add_axioms_for_is_prefix(), add_axioms_for_last_index_of(), add_axioms_for_last_index_of_string(), and add_axioms_for_trim().
|
private |
construct a string expression whose length and content are new variables
Definition at line 164 of file string_constraint_generator_main.cpp.
References char_type(), created_strings, fresh_symbol, index_type(), and to_array_string_expr().
Referenced by add_axioms_for_concat_code_point(), add_axioms_for_delete(), add_axioms_for_format(), add_axioms_for_format_specifier(), add_axioms_for_insert(), add_axioms_for_insert_char(), add_axioms_for_string_of_float(), and add_axioms_from_float_scientific_notation().
symbol_exprt string_constraint_generatort::fresh_univ_index | ( | const irep_idt & | prefix, |
const typet & | type | ||
) |
generate an index symbol to be used as an universaly quantified variable
Definition at line 104 of file string_constraint_generator_main.cpp.
References fresh_symbol.
Referenced by add_axioms_for_compare_to(), add_axioms_for_concat_char(), add_axioms_for_concat_substr(), add_axioms_for_contains(), add_axioms_for_equals(), add_axioms_for_equals_ignore_case(), add_axioms_for_index_of(), add_axioms_for_index_of_string(), add_axioms_for_is_prefix(), add_axioms_for_last_index_of(), add_axioms_for_last_index_of_string(), add_axioms_for_replace(), add_axioms_for_set_char(), add_axioms_for_set_length(), add_axioms_for_substring(), add_axioms_for_to_lower_case(), add_axioms_for_to_upper_case(), add_axioms_for_trim(), add_constraint_on_characters(), and check_axioms().
const std::vector< symbol_exprt > & string_constraint_generatort::get_boolean_symbols | ( | ) | const |
Boolean symbols for the results of some string functions.
Definition at line 65 of file string_constraint_generator_main.cpp.
References boolean_symbols.
Referenced by check_axioms().
const std::vector< string_constraintt > & string_constraint_generatort::get_constraints | ( | ) | const |
Definition at line 47 of file string_constraint_generator_main.cpp.
References constraints.
Referenced by string_refinementt::dec_solve().
const std::set< array_string_exprt > & string_constraint_generatort::get_created_strings | ( | ) | const |
Set of strings that have been created by the generator.
Definition at line 71 of file string_constraint_generator_main.cpp.
References created_strings.
Referenced by string_refinementt::get().
const std::vector< symbol_exprt > & string_constraint_generatort::get_index_symbols | ( | ) | const |
Symbols used in existential quantifications.
Definition at line 59 of file string_constraint_generator_main.cpp.
References index_symbols.
Referenced by check_axioms().
const std::vector< exprt > & string_constraint_generatort::get_lemmas | ( | ) | const |
Axioms are of three kinds: universally quantified string constraint, not contains string constraints and simple formulas.
Definition at line 36 of file string_constraint_generator_main.cpp.
References lemmas.
Referenced by string_refinementt::dec_solve().
const std::vector< string_not_contains_constraintt > & string_constraint_generatort::get_not_contains_constraints | ( | ) | const |
Definition at line 53 of file string_constraint_generator_main.cpp.
References not_contains_constraints.
Referenced by string_refinementt::dec_solve().
|
inline |
Definition at line 144 of file string_constraint_generator.h.
Referenced by add_axioms_for_code_point(), add_axioms_for_concat_char(), add_axioms_for_concat_substr(), add_axioms_for_constant(), add_axioms_for_constrain_characters(), add_axioms_for_cprover_string(), add_axioms_for_empty_string(), add_axioms_for_format(), add_axioms_for_insert(), add_axioms_for_set_char(), add_axioms_for_to_lower_case(), add_axioms_for_to_upper_case(), and add_axioms_from_char().
|
private |
casts an expression to a string expression, or fetches the actual string_exprt in the case of a symbol.
expr | an expression of refined string type |
Definition at line 283 of file string_constraint_generator_main.cpp.
References char_array_of_pointer(), refined_string_exprt::content(), is_refined_string_type(), refined_string_exprt::length(), PRECONDITION, to_string_expr(), and exprt::type().
Referenced by add_axioms_for_char_at(), add_axioms_for_char_set(), add_axioms_for_code_point_at(), add_axioms_for_code_point_before(), add_axioms_for_code_point_count(), add_axioms_for_compare_to(), add_axioms_for_concat(), add_axioms_for_concat_char(), add_axioms_for_concat_code_point(), add_axioms_for_contains(), add_axioms_for_delete(), add_axioms_for_delete_char_at(), add_axioms_for_equals(), add_axioms_for_equals_ignore_case(), add_axioms_for_format(), add_axioms_for_format_specifier(), add_axioms_for_hash_code(), add_axioms_for_index_of(), add_axioms_for_insert(), add_axioms_for_insert_char(), add_axioms_for_is_prefix(), add_axioms_for_last_index_of(), add_axioms_for_length(), add_axioms_for_parse_int(), add_axioms_for_replace(), add_axioms_for_set_length(), add_axioms_for_substring(), add_axioms_for_to_lower_case(), add_axioms_for_to_upper_case(), and add_axioms_for_trim().
|
inline |
Definition at line 119 of file string_constraint_generator.h.
References witness.
Referenced by check_axioms(), and string_refinementt::instantiate_not_contains().
Returns the integer value represented by the character.
chr | a character expression in the following set: 0123456789abcdef |
Definition at line 191 of file string_constraint_generator_valueof.cpp.
References constant_char(), and exprt::type().
the output is true when the character is a high surrogate for UTF-16 encoding, see https://en.wikipedia.org/wiki/UTF-16 for more explenation about the encoding; this is true when the character is in the range 0xD800..0xDBFF
chr | a character expression |
Definition at line 75 of file string_constraint_generator_code_points.cpp.
References constant_char(), and exprt::type().
Referenced by add_axioms_for_code_point_at(), and add_axioms_for_code_point_before().
the output is true when the character is a low surrogate for UTF-16 encoding, see https://en.wikipedia.org/wiki/UTF-16 for more explenation about the encoding; this is true when the character is in the range 0xDC00..0xDFFF
chr | a character expression |
Definition at line 88 of file string_constraint_generator_code_points.cpp.
References constant_char(), and exprt::type().
Referenced by add_axioms_for_code_point_at(), and add_axioms_for_code_point_before().
optionalt< exprt > string_constraint_generatort::make_array_pointer_association | ( | const function_application_exprt & | expr | ) |
Associate array to pointer, and array to length.
Definition at line 395 of file string_constraint_generator_main.cpp.
References associate_array_to_pointer(), associate_length_to_array(), and get_function_name().
Referenced by make_char_array_pointer_associations().
|
private |
If the expression is a constant expression then we get the value of it as an unsigned long.
If not we return a default value.
expr | input expression |
def | default value to return if we cannot evaluate expr |
Definition at line 541 of file string_constraint_generator_valueof.cpp.
References integer2ulong(), ns, simplify_expr(), and to_integer().
Referenced by add_axioms_for_parse_int(), and add_axioms_for_string_of_int_with_radix().
array_poolt string_constraint_generatort::array_pool |
Definition at line 135 of file string_constraint_generator.h.
Referenced by associate_array_to_pointer(), associate_length_to_array(), char_array_of_pointer(), debug_model(), string_refinementt::dec_solve(), and string_refinementt::get().
|
private |
Definition at line 413 of file string_constraint_generator.h.
Referenced by fresh_boolean(), and get_boolean_symbols().
|
private |
Definition at line 411 of file string_constraint_generator.h.
Referenced by add_axioms_for_compare_to(), add_axioms_for_concat_char(), add_axioms_for_concat_substr(), add_axioms_for_contains(), add_axioms_for_equals(), add_axioms_for_equals_ignore_case(), add_axioms_for_index_of(), add_axioms_for_index_of_string(), add_axioms_for_insert(), add_axioms_for_is_prefix(), add_axioms_for_last_index_of(), add_axioms_for_last_index_of_string(), add_axioms_for_replace(), add_axioms_for_set_char(), add_axioms_for_set_length(), add_axioms_for_substring(), add_axioms_for_to_lower_case(), add_axioms_for_to_upper_case(), add_axioms_for_trim(), add_constraint_on_characters(), clear_constraints(), and get_constraints().
|
private |
Definition at line 407 of file string_constraint_generator.h.
Referenced by associate_array_to_pointer(), char_array_of_pointer(), fresh_string(), and get_created_strings().
symbol_generatort string_constraint_generatort::fresh_symbol |
Definition at line 129 of file string_constraint_generator.h.
Referenced by add_axioms_for_char_at(), add_axioms_for_code_point_at(), add_axioms_for_code_point_before(), add_axioms_for_code_point_count(), add_axioms_for_compare_to(), add_axioms_for_hash_code(), add_axioms_for_insert(), add_axioms_for_offset_by_code_point(), add_axioms_for_parse_int(), check_axioms(), string_refinementt::dec_solve(), fresh_boolean(), fresh_exist_index(), fresh_string(), and fresh_univ_index().
|
private |
Definition at line 418 of file string_constraint_generator.h.
Referenced by add_axioms_for_hash_code().
|
private |
Definition at line 414 of file string_constraint_generator.h.
Referenced by fresh_exist_index(), and get_index_symbols().
|
private |
Definition at line 421 of file string_constraint_generator.h.
|
private |
Definition at line 410 of file string_constraint_generator.h.
Referenced by add_axioms_for_char_at(), add_axioms_for_characters_in_integer_string(), add_axioms_for_code_point(), add_axioms_for_code_point_at(), add_axioms_for_code_point_before(), add_axioms_for_code_point_count(), add_axioms_for_compare_to(), add_axioms_for_concat_char(), add_axioms_for_concat_substr(), add_axioms_for_constant(), add_axioms_for_contains(), add_axioms_for_correct_number_format(), add_axioms_for_empty_string(), add_axioms_for_equals(), add_axioms_for_equals_ignore_case(), add_axioms_for_format(), add_axioms_for_fractional_part(), add_axioms_for_hash_code(), add_axioms_for_index_of(), add_axioms_for_index_of_string(), add_axioms_for_insert(), add_axioms_for_is_prefix(), add_axioms_for_last_index_of(), add_axioms_for_last_index_of_string(), add_axioms_for_offset_by_code_point(), add_axioms_for_replace(), add_axioms_for_set_char(), add_axioms_for_set_length(), add_axioms_for_substring(), add_axioms_for_to_lower_case(), add_axioms_for_to_upper_case(), add_axioms_for_trim(), add_axioms_from_char(), add_lemma(), associate_length_to_array(), clear_constraints(), and get_lemmas().
|
private |
Definition at line 408 of file string_constraint_generator.h.
Referenced by add_axioms_for_format(), and add_axioms_for_format_specifier().
|
private |
Definition at line 412 of file string_constraint_generator.h.
Referenced by add_axioms_for_contains(), add_axioms_for_index_of_string(), add_axioms_for_last_index_of_string(), clear_constraints(), and get_not_contains_constraints().
|
private |
Definition at line 415 of file string_constraint_generator.h.
Referenced by to_integer_or_default().
std::map<string_not_contains_constraintt, symbol_exprt> string_constraint_generatort::witness |
Definition at line 405 of file string_constraint_generator.h.
Referenced by add_axioms_for_equals(), add_axioms_for_equals_ignore_case(), add_axioms_for_is_prefix(), string_refinementt::dec_solve(), and get_witness_of().