cprover
Loading...
Searching...
No Matches
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)
void merge (string_constraintst &result, string_constraintst other)
 Merge two sets of constraints by appending to the first one.
signedbv_typet get_return_code_type ()
static irep_idt get_function_name (const function_application_exprt &expr)
exprt is_positive (const exprt &x)
exprt minimum (const exprt &a, const exprt &b)
exprt maximum (const exprt &a, const exprt &b)
exprt zero_if_negative (const exprt &expr)
 Returns a non-negative version of the argument.

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

irep_idt get_function_name ( const function_application_exprt & expr)
static

Definition at line 187 of file string_constraint_generator_main.cpp.

◆ get_return_code_type()

signedbv_typet get_return_code_type ( )

Definition at line 182 of file string_constraint_generator_main.cpp.

◆ is_positive()

exprt is_positive ( const exprt & x)
Parameters
xan expression
Returns
a Boolean expression true exactly when x is positive

Definition at line 341 of file string_constraint_generator_main.cpp.

◆ maximum()

exprt maximum ( const exprt & a,
const exprt & b )
Returns
expression representing the maximum of two expressions

Definition at line 404 of file string_constraint_generator_main.cpp.

◆ merge()

void merge ( string_constraintst & result,
string_constraintst other )

Merge two sets of constraints by appending to the first one.

Definition at line 101 of file string_constraint_generator_main.cpp.

◆ minimum()

exprt minimum ( const exprt & a,
const exprt & b )
Returns
expression representing the minimum of two expressions

Definition at line 399 of file string_constraint_generator_main.cpp.

◆ sum_overflows()

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

Definition at line 40 of file string_constraint_generator_main.cpp.

◆ zero_if_negative()

exprt zero_if_negative ( const exprt & expr)

Returns a non-negative version of the argument.

Parameters
exprexpression of which we want a non-negative version
Returns
max(0, expr)

Definition at line 412 of file string_constraint_generator_main.cpp.