cprover
string_constraint_generator_insert.cpp File Reference

Generates string constraints for the family of insert Java functions. More...

+ Include dependency graph for string_constraint_generator_insert.cpp:

Go to the source code of this file.

Functions

std::pair< exprt, string_constraintstadd_axioms_for_insert (symbol_generatort &fresh_symbol, 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 length_constraint_for_insert (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
 Add axioms ensuring the length of res corresponds to that of s1 where we inserted s2. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_insert (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool)
 Insertion of a string in another at a specific index. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_insert_int (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
 add axioms corresponding to the StringBuilder.insert(I) java function More...
 
std::pair< exprt, string_constraintstadd_axioms_for_insert_bool (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 add axioms corresponding to the StringBuilder.insert(Z) java function More...
 
std::pair< exprt, string_constraintstadd_axioms_for_insert_char (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
 Add axioms corresponding to the StringBuilder.insert(C) java function. More...
 
std::pair< exprt, string_constraintstadd_axioms_for_insert_double (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
 add axioms corresponding to the StringBuilder.insert(D) java function More...
 
std::pair< exprt, string_constraintstadd_axioms_for_insert_float (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
 Add axioms corresponding to the StringBuilder.insert(F) java function. More...
 

Detailed Description

Generates string constraints for the family of insert Java functions.

Definition in file string_constraint_generator_insert.cpp.

Function Documentation

◆ add_axioms_for_insert() [1/2]

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

  1. res.length = s1.length + s2.length
  2. forall i < offset' . res[i] = s1[i]
  3. forall i < s2.length. res[i + offset'] = s2[i]
  4. forall i in [offset', s1.length). res[i + s2.length] = s1[i] This is equivalent to ‘res=concat(substring(s1, 0, offset’), concat(s2, substring(s1, offset')))`.
    Parameters
    fresh_symbolgenerator of fresh symbols
    resarray of characters expression
    s1array of characters expression
    s2array of characters expression
    offsetinteger expression
    Returns
    an expression expression which is different from zero if there is an exception to signal

Definition at line 33 of file string_constraint_generator_insert.cpp.

◆ add_axioms_for_insert() [2/2]

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

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.

Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with arguments integer |res|, character pointer &res[0], refined_string s1, refined_strings2, integer offset, optional integer start and optional integer end
poolpool of arrays representing strings
Returns
an integer expression which is different from zero if there is an exception to signal

Definition at line 106 of file string_constraint_generator_insert.cpp.

◆ add_axioms_for_insert_bool()

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

add axioms corresponding to the StringBuilder.insert(Z) java function

Deprecated:
should convert the value to string and call insert
Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with three arguments: a string, an integer offset, and a Boolean
array_poolpool of arrays representing strings
Returns
a new string expression

Definition at line 171 of file string_constraint_generator_insert.cpp.

◆ add_axioms_for_insert_char()

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

Add axioms corresponding to the StringBuilder.insert(C) java function.

Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with three arguments: a string, an integer offset, and a character
array_poolpool of arrays representing strings
Returns
an expression

Definition at line 196 of file string_constraint_generator_insert.cpp.

◆ add_axioms_for_insert_double()

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

add axioms corresponding to the StringBuilder.insert(D) java function

Deprecated:
should convert the value to string and call insert
Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with three arguments: a string, an integer offset, and a double
array_poolpool of arrays representing strings
nsnamespace
Returns
a string expression

Definition at line 223 of file string_constraint_generator_insert.cpp.

◆ add_axioms_for_insert_float()

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

Add axioms corresponding to the StringBuilder.insert(F) java function.

Deprecated:
should convert the value to string and call insert
Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with three arguments: a string, an integer offset, and a float
array_poolpool of arrays representing strings
nsnamespace
Returns
a new string expression

Definition at line 252 of file string_constraint_generator_insert.cpp.

◆ add_axioms_for_insert_int()

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

add axioms corresponding to the StringBuilder.insert(I) java function

Deprecated:
should convert the value to string and call insert
Parameters
fresh_symbolgenerator of fresh symbols
ffunction application with three arguments: a string, an integer offset, and an integer
array_poolpool of arrays representing strings
nsnamespace
Returns
an expression

Definition at line 144 of file string_constraint_generator_insert.cpp.

◆ length_constraint_for_insert()

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

Add axioms ensuring the length of res corresponds to that of s1 where we inserted s2.

Definition at line 80 of file string_constraint_generator_insert.cpp.