cprover
string_constraint_generator_main.cpp File Reference

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

#include "string_constraint_generator.h"
#include "string_refinement_invariant.h"
#include <iterator>
#include <limits>
#include <util/arith_tools.h>
#include <util/deprecate.h>
#include <util/interval_constraint.h>
#include <util/pointer_predicates.h>
#include <util/simplify_expr.h>
#include <util/ssa_expr.h>
#include <util/string_constant.h>
+ 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 185 of file string_constraint_generator_main.cpp.

◆ get_return_code_type()

signedbv_typet get_return_code_type ( )

Definition at line 180 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 338 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 400 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 100 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 395 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 39 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 408 of file string_constraint_generator_main.cpp.