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)
 Add axioms ensuring the length of res corresponds to that of s1 where we inserted s2. 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 
)

Add axioms ensuring the length of res corresponds to that of s1 where we inserted s2.

Definition at line 76 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().