cprover
|
String expressions for the string solver. More...
Go to the source code of this file.
Classes | |
class | string_exprt< child_t > |
class | array_string_exprt |
class | refined_string_exprt |
Functions | |
array_string_exprt & | to_array_string_expr (exprt &expr) |
const array_string_exprt & | to_array_string_expr (const exprt &expr) |
refined_string_exprt & | to_string_expr (exprt &expr) |
const refined_string_exprt & | to_string_expr (const exprt &expr) |
template<> | |
bool | can_cast_expr< refined_string_exprt > (const exprt &base) |
void | validate_expr (const refined_string_exprt &x) |
String expressions for the string solver.
Definition in file string_expr.h.
|
inline |
Definition at line 245 of file string_expr.h.
|
inline |
Definition at line 162 of file string_expr.h.
References irept::id(), PRECONDITION, and exprt::type().
Referenced by string_constraint_generatort::associate_array_to_pointer(), string_constraint_generatort::associate_length_to_array(), eval_string(), for_each_atomic_string(), string_dependenciest::for_each_dependency(), string_constraint_generatort::fresh_string(), string_refinementt::get(), get_char_array_and_concretize(), array_poolt::make_char_array_for_char_pointer(), make_string(), string_not_contains_constraintt::s0(), and string_not_contains_constraintt::s1().
|
inline |
Definition at line 168 of file string_expr.h.
References irept::id(), PRECONDITION, and exprt::type().
|
inline |
Definition at line 230 of file string_expr.h.
References irept::id(), exprt::operands(), and PRECONDITION.
Referenced by string_constraint_generatort::get_string_expr(), java_string_library_preprocesst::make_argument_for_format(), and java_string_library_preprocesst::make_init_from_array_code().
|
inline |
Definition at line 237 of file string_expr.h.
References irept::id(), exprt::operands(), and PRECONDITION.
|
inline |
Definition at line 250 of file string_expr.h.
References refined_string_exprt::content(), irept::id(), INVARIANT, refined_string_exprt::length(), exprt::type(), and validate_operands().