string_concatenation_builtin_function.cpp File Reference

Builtin functions for string concatenations. More...

#include "string_concatenation_builtin_function.h"
#include <algorithm>

Include dependency graph for string_concatenation_builtin_function.cpp:

Go to the source code of this file.

Functions
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, array_poolt &array_pool)
	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'‘.
exprt	length_constraint_for_concat (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, array_poolt &array_pool)
	Add axioms enforcing that the length of res is that of the concatenation of s1 with s2
exprt	length_constraint_for_concat_char (const array_string_exprt &res, const array_string_exprt &s1, array_poolt &array_pool)
	Add axioms enforcing that the length of res is that of the concatenation of s1 with.

Detailed Description

Builtin functions for string concatenations.

Definition in file string_concatenation_builtin_function.cpp.

Function Documentation

length_constraint_for_concat()

exprt length_constraint_for_concat	(	const array_string_exprt &	res,
		const array_string_exprt &	s1,
		const array_string_exprt &	s2,
		array_poolt &	array_pool
	)

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

Definition at line 125 of file string_concatenation_builtin_function.cpp.

length_constraint_for_concat_char()

exprt length_constraint_for_concat_char	(	const array_string_exprt &	res,
		const array_string_exprt &	s1,
		array_poolt &	array_pool
	)

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

Definition at line 140 of file string_concatenation_builtin_function.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,
		array_poolt &	array_pool
	)

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 102 of file string_concatenation_builtin_function.cpp.