cprover
string_constraint_generator_concat.cpp File Reference

Generates string constraints for functions adding content add the end of strings. More...

+ Include dependency graph for string_constraint_generator_concat.cpp:

Go to the source code of this file.

Functions

std::pair< exprt, string_constraintstadd_axioms_for_concat_substr (symbol_generatort &fresh_symbol, 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 indexend_index'`. More...
 
exprt length_constraint_for_concat_substr (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &start, const exprt &end)
 Add axioms enforcing that the length of res is that of the concatenation of s1 with the substring of s2 starting at index ‘start’ and ending at indexend'`. More...
 
exprt length_constraint_for_concat (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
 Add axioms enforcing that the length of res is that of the concatenation of s1 with s2 More...
 
exprt length_constraint_for_concat_char (const array_string_exprt &res, const array_string_exprt &s1)
 Add axioms enforcing that the length of res is that of the concatenation of s1 with. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_concat (symbol_generatort &fresh_symbol, 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...
 
std::pair< exprt, string_constraintstadd_axioms_for_concat_code_point (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 Add axioms corresponding to the StringBuilder.appendCodePoint(I) function. More...
 

Detailed Description

Generates string constraints for functions adding content add the end of strings.

Definition in file string_constraint_generator_concat.cpp.

Function Documentation

◆ add_axioms_for_concat()

std::pair<exprt, string_constraintst> add_axioms_for_concat ( symbol_generatort fresh_symbol,
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.

Deprecated:
should use concat_substr instead
Parameters
fresh_symbolgenerator of fresh symbols
resstring_expression corresponding to the result
s1the string expression to append to
s2the string expression to append to the first one
Returns
an integer expression

Definition at line 126 of file string_constraint_generator_concat.cpp.

◆ add_axioms_for_concat_code_point()

std::pair<exprt, string_constraintst> add_axioms_for_concat_code_point ( symbol_generatort fresh_symbol,
const function_application_exprt f,
array_poolt array_pool 
)

Add axioms corresponding to the StringBuilder.appendCodePoint(I) function.

Deprecated:
java specific
Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with two arguments: a string and a code point
array_poolpool of arrays representing strings
Returns
an expression

Definition at line 143 of file string_constraint_generator_concat.cpp.

◆ add_axioms_for_concat_substr()

std::pair<exprt, string_constraintst> add_axioms_for_concat_substr ( symbol_generatort fresh_symbol,
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 indexend_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:

  1. \(|res| = overflow ? |s_1| + end\_index' - start\_index' : max_int \)
  2. \(\forall i<|s_1|. res[i]=s_1[i] \)
  3. \(\forall i< |res| - |s_1|.\ res[i+|s_1|] = s_2[start\_index'+i]\)
Parameters
fresh_symbolgenerator of fresh symbols
resan array of characters expression
s1an array of characters expression
s2an array of characters expression
start_indexinteger expression
end_indexinteger expression
Returns
integer expression 0

Definition at line 38 of file string_constraint_generator_concat.cpp.

◆ length_constraint_for_concat()

exprt length_constraint_for_concat ( const array_string_exprt res,
const array_string_exprt s1,
const array_string_exprt s2 
)

Add axioms enforcing that the length of res is that of the concatenation of s1 with s2

Definition at line 99 of file string_constraint_generator_concat.cpp.

◆ length_constraint_for_concat_char()

exprt length_constraint_for_concat_char ( const array_string_exprt res,
const array_string_exprt s1 
)

Add axioms enforcing that the length of res is that of the concatenation of s1 with.

Definition at line 109 of file string_constraint_generator_concat.cpp.

◆ length_constraint_for_concat_substr()

exprt length_constraint_for_concat_substr ( const array_string_exprt res,
const array_string_exprt s1,
const array_string_exprt s2,
const exprt start,
const exprt end 
)

Add axioms enforcing that the length of res is that of the concatenation of s1 with the substring of s2 starting at index ‘start’ and ending at indexend'`.

Where start_index' is max(0, start) and end' is max(min(end, s2.length), start')

Definition at line 81 of file string_constraint_generator_concat.cpp.