CBMC
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. More...
 
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. More...
 

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

static 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.