Go to the documentation of this file.
12 #ifndef CPROVER_UTIL_STRING_EXPR_H
13 #define CPROVER_UTIL_STRING_EXPR_H
104 return static_cast<array_string_exprt &>(expr);
110 return static_cast<const array_string_exprt &>(expr);
122 const exprt &_length,
123 const exprt &_content,
165 return static_cast<refined_string_exprt &>(expr);
172 return static_cast<const refined_string_exprt &>(expr);
178 return base.
id() == ID_struct && base.
operands().size() == 2;
183 INVARIANT(x.
id() == ID_struct,
"refined string exprs are struct");
186 x.
length().
type().
id() == ID_signedbv,
"length should be a signed int");
#define PRECONDITION(CONDITION)
exprt operator[](const exprt &i) const
binary_relation_exprt length_ge(const T &lhs, const exprt &rhs)
equal_exprt length_eq(const T &lhs, const exprt &rhs)
refined_string_exprt(const exprt &_length, const exprt &_content, const typet &type)
refined_string_exprt & to_string_expr(exprt &expr)
The type of an expression, extends irept.
const exprt & length() const
binary_relation_exprt length_gt(const T &lhs, const exprt &rhs)
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
void validate_expr(const refined_string_exprt &x)
Base class for all expressions.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
bool can_cast_expr< refined_string_exprt >(const exprt &base)
const exprt & content() const
const exprt & length() const
Struct constructor from list of elements.
const exprt & size() const
typet & type()
Return the type of the expression.
refined_string_exprt(const exprt &_length, const exprt &_content)
const irep_idt & id() const
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
array_string_exprt & to_array_string_expr(exprt &expr)
binary_relation_exprt length_le(const T &lhs, const exprt &rhs)
const exprt & content() const
A base class for relations, i.e., binary predicates.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
index_exprt operator[](int i) const
friend refined_string_exprt & to_string_expr(exprt &expr)