cprover
string_constraint_generator_concat.cpp File Reference

Generates string constraints for functions adding content add the end of strings. More...

Include dependency graph for string_constraint_generator_concat.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)
 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'`. More...
 
exprt length_constraint_for_concat (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
 Add axioms enforcing that the length of res is that of the concatenation of s1 with s2 More...
 
exprt length_constraint_for_concat_char (const array_string_exprt &res, const array_string_exprt &s1)
 Add axioms enforcing that the length of res is that of the concatenation of s1 with. More...
 

Detailed Description

Generates string constraints for functions adding content add the end of strings.

Definition in file string_constraint_generator_concat.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 
)

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

Definition at line 95 of file string_constraint_generator_concat.cpp.

References array_string_exprt::length().

Referenced by string_concatenation_builtin_functiont::length_constraint().

◆ length_constraint_for_concat_char()

exprt length_constraint_for_concat_char ( const array_string_exprt res,
const array_string_exprt s1 
)

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

Definition at line 135 of file string_constraint_generator_concat.cpp.

References from_integer(), and array_string_exprt::length().

Referenced by string_constraint_generatort::add_axioms_for_concat_char(), and string_concat_char_builtin_functiont::length_constraint().

◆ 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 
)

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 77 of file string_constraint_generator_concat.cpp.

References from_integer(), irept::id(), array_string_exprt::length(), maximum(), minimum(), PRECONDITION, sum_overflows(), to_signedbv_type(), and exprt::type().

Referenced by string_constraint_generatort::add_axioms_for_concat_substr(), and string_concatenation_builtin_functiont::length_constraint().