cprover
Loading...
Searching...
No Matches
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 index end'‘.
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 index end'‘.

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.