Loading...

Searching...

No Matches

Functions

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.