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 <util/arith_tools.h>
#include <util/deprecate.h>
#include <util/interval_constraint.h>
#include <util/mathematical_expr.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.