cprover
string_constraint_generator_main.cpp File Reference

Generates string constraints to link results from string functions with their arguments. More...

Include dependency graph for string_constraint_generator_main.cpp:

Go to the source code of this file.

Functions

exprt sum_overflows (const plus_exprt &sum)
 
static irep_idt get_function_name (const function_application_exprt &expr)
 
exprt minimum (const exprt &a, const exprt &b)
 
exprt maximum (const exprt &a, const exprt &b)
 

Detailed Description

Generates string constraints to link results from string functions with their arguments.

This is inspired by the PASS paper at HVC'13: "PASS: String Solving with Parameterized Array and Interval Automaton" by Guodong Li and Indradeep Ghosh, which gives examples of constraints for several functions.

Definition in file string_constraint_generator_main.cpp.

Function Documentation

◆ get_function_name()

◆ maximum()

◆ minimum()

◆ sum_overflows()

exprt sum_overflows ( const plus_exprt sum)
Returns
Boolean true when the sum of the two expressions overflows

Definition at line 132 of file string_constraint_generator_main.cpp.

References from_integer(), exprt::op0(), exprt::op1(), exprt::operands(), PRECONDITION, and exprt::type().

Referenced by length_constraint_for_concat_substr().