Go to the documentation of this file.
9 #ifndef CPROVER_ANSI_C_C_EXPR_H
10 #define CPROVER_ANSI_C_C_EXPR_H
78 return base.
id() == ID_shuffle_vector;
127 {std::move(_lhs), std::move(_rhs), std::move(_result)},
167 if(base.
id() != ID_side_effect)
171 return statement == ID_overflow_plus || statement == ID_overflow_mult ||
172 statement == ID_overflow_minus;
186 side_effect_expr.get_statement() == ID_overflow_plus ||
187 side_effect_expr.get_statement() == ID_overflow_mult ||
188 side_effect_expr.get_statement() == ID_overflow_minus);
197 side_effect_expr.get_statement() == ID_overflow_plus ||
198 side_effect_expr.get_statement() == ID_overflow_mult ||
199 side_effect_expr.get_statement() == ID_overflow_minus);
228 #endif // CPROVER_ANSI_C_C_EXPR_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A base class for multi-ary expressions Associativity is not specified.
const side_effect_expr_overflowt & to_side_effect_expr_overflow(const exprt &expr)
Cast an exprt to a side_effect_expr_overflowt.
const history_exprt & to_history_expr(const exprt &expr, const irep_idt &id)
Shuffle elements of one or two vectors, modelled after Clang's __builtin_shufflevector.
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
const exprt & lhs() const
Base class for all expressions.
Generic base class for unary expressions.
const vector_typet & type() const
Vector constructor from list of elements.
side_effect_exprt & to_side_effect_expr(exprt &expr)
const exprt & vector2() const
void validate_expr(const shuffle_vector_exprt &value)
typet & type()
Return the type of the expression.
const std::string & id2string(const irep_idt &d)
#define PRECONDITION(CONDITION)
side_effect_expr_overflowt(const irep_idt &kind, exprt _lhs, exprt _rhs, exprt _result, const source_locationt &loc)
const shuffle_vector_exprt & to_shuffle_vector_expr(const exprt &expr)
Cast an exprt to a shuffle_vector_exprt.
const irep_idt & id() const
std::vector< exprt > operandst
nonstd::optional< T > optionalt
bool can_cast_expr< shuffle_vector_exprt >(const exprt &base)
vector_exprt lower() const
const irep_idt & get_statement() const
exprt::operandst & indices()
bool can_cast_expr< side_effect_expr_overflowt >(const exprt &base)
const exprt::operandst & indices() const
A class for an expression that indicates a history variable.
const exprt & vector1() const
history_exprt(exprt variable, const irep_idt &id)
A Boolean expression returning true, iff the result of performing operation kind on operands a and b ...
const exprt & rhs() const
bool has_two_input_vectors() const
const exprt & expression() const
const exprt & result() const
shuffle_vector_exprt(exprt vector1, optionalt< exprt > vector2, exprt::operandst indices)
An expression containing a side effect.