cprover
|
Generates string constraints to link results from string functions with their arguments. More...
#include <solvers/refinement/string_constraint_generator.h>
#include <limits>
#include <solvers/refinement/string_refinement_invariant.h>
#include <util/arith_tools.h>
#include <util/pointer_predicates.h>
#include <util/ssa_expr.h>
#include <util/string_constant.h>
#include <util/deprecate.h>
Go to the source code of this file.
Functions | |
exprt | sum_overflows (const plus_exprt &sum) |
static irep_idt | get_function_name (const function_application_exprt &expr) |
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... | |
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.
|
static |
Definition at line 387 of file string_constraint_generator_main.cpp.
References function_application_exprt::function(), symbol_exprt::get_identifier(), ssa_exprt::get_object_name(), irept::id(), is_ssa_expr(), PRECONDITION, to_ssa_expr(), and to_symbol_expr().
Referenced by string_constraint_generatort::add_axioms_for_function_application(), and string_constraint_generatort::make_array_pointer_association().
Definition at line 615 of file string_constraint_generator_main.cpp.
Referenced by string_constraint_generatort::add_axioms_for_concat_substr(), string_constraint_generatort::add_axioms_for_insert(), string_constraint_generatort::add_axioms_for_is_prefix(), string_constraint_generatort::add_axioms_for_offset_by_code_point(), string_constraint_generatort::add_axioms_for_substring(), length_constraint_for_concat_substr(), and zero_if_negative().
Definition at line 610 of file string_constraint_generator_main.cpp.
Referenced by string_constraint_generatort::add_axioms_for_code_point_count(), string_constraint_generatort::add_axioms_for_concat_substr(), string_constraint_generatort::add_axioms_for_insert(), string_constraint_generatort::add_axioms_for_offset_by_code_point(), string_constraint_generatort::add_axioms_for_set_char(), string_constraint_generatort::add_axioms_for_set_length(), string_constraint_generatort::add_axioms_for_substring(), and length_constraint_for_concat_substr().
exprt sum_overflows | ( | const plus_exprt & | sum | ) |
Definition at line 132 of file string_constraint_generator_main.cpp.
References from_integer(), exprt::op0(), exprt::op1(), exprt::operands(), PRECONDITION, and exprt::type().
Referenced by length_constraint_for_concat_substr().
Returns a non-negative version of the argument.
expr | expression of which we want a non-negative version |
max(0, expr)
Definition at line 623 of file string_constraint_generator_main.cpp.
References from_integer(), maximum(), and exprt::type().
Referenced by string_constraint_generatort::add_axioms_for_compare_to(), string_constraint_generatort::add_axioms_for_concat_char(), string_constraint_generatort::add_axioms_for_concat_substr(), string_constraint_generatort::add_axioms_for_contains(), string_constraint_generatort::add_axioms_for_equals(), string_constraint_generatort::add_axioms_for_equals_ignore_case(), string_constraint_generatort::add_axioms_for_index_of(), string_constraint_generatort::add_axioms_for_index_of_string(), string_constraint_generatort::add_axioms_for_insert(), string_constraint_generatort::add_axioms_for_is_suffix(), string_constraint_generatort::add_axioms_for_last_index_of(), string_constraint_generatort::add_axioms_for_last_index_of_string(), string_constraint_generatort::add_axioms_for_replace(), string_constraint_generatort::add_axioms_for_set_char(), string_constraint_generatort::add_axioms_for_set_length(), string_constraint_generatort::add_axioms_for_substring(), string_constraint_generatort::add_axioms_for_to_lower_case(), string_constraint_generatort::add_axioms_for_to_upper_case(), string_constraint_generatort::add_axioms_for_trim(), and string_constraint_generatort::add_constraint_on_characters().