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

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.