cprover
string_constraint_generator_insert.cpp File Reference

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

Include dependency graph for string_constraint_generator_insert.cpp:

Go to the source code of this file.

Functions

exprt length_constraint_for_insert (const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &offset)
 Add axioms ensuring the length of res corresponds that of s1 where we inserted s2 at position offset. More...
 

Detailed Description

Generates string constraints for the family of insert Java functions.

Definition in file string_constraint_generator_insert.cpp.

Function Documentation

◆ length_constraint_for_insert()

exprt length_constraint_for_insert ( const array_string_exprt res,
const array_string_exprt s1,
const array_string_exprt s2,
const exprt offset 
)

Add axioms ensuring the length of res corresponds that of s1 where we inserted s2 at position offset.

Definition at line 74 of file string_constraint_generator_insert.cpp.

References array_string_exprt::length().

Referenced by string_constraint_generatort::add_axioms_for_insert(), and string_insertion_builtin_functiont::length_constraint().