string_constraint_generator_insert.cpp File Reference

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

#include <solvers/refinement/string_refinement_invariant.h>
#include <solvers/refinement/string_constraint_generator.h>
#include <util/deprecate.h>

Include dependency graph for string_constraint_generator_insert.cpp:

Go to the source code of this file.

Functions
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. 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_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. More...
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 More...
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 More...
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. More...
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 More...
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. 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_symbol	generator of fresh symbols
   res	array of characters expression
   s1	array of characters expression
   s2	array of characters expression
   offset	integer 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_symbol	generator of fresh symbols
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
pool	pool 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_symbol	generator of fresh symbols
f	function application with three arguments: a string, an integer offset, and a Boolean
array_pool	pool 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_symbol	generator of fresh symbols
f	function application with three arguments: a string, an integer offset, and a character
array_pool	pool 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_symbol	generator of fresh symbols
f	function application with three arguments: a string, an integer offset, and a double
array_pool	pool of arrays representing strings
ns	namespace

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_symbol	generator of fresh symbols
f	function application with three arguments: a string, an integer offset, and a float
array_pool	pool of arrays representing strings
ns	namespace

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_symbol	generator of fresh symbols
f	function application with three arguments: a string, an integer offset, and an integer
array_pool	pool of arrays representing strings
ns	namespace

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.