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);
248 "conditional target expression must have two operands");
252 expr.
operands()[1].id() == ID_expression_list,
253 "conditional target second operand must be an ID_expression_list "
254 "expression, found " +
295 return base.
id() == ID_conditional_target_group;
bool can_cast_expr< side_effect_expr_overflowt >(const exprt &base)
const shuffle_vector_exprt & to_shuffle_vector_expr(const exprt &expr)
Cast an exprt to a shuffle_vector_exprt.
const conditional_target_group_exprt & to_conditional_target_group_expr(const exprt &expr)
Cast an exprt to a conditional_target_group_exprt.
bool can_cast_expr< conditional_target_group_exprt >(const exprt &base)
const history_exprt & to_history_expr(const exprt &expr, const irep_idt &id)
void validate_expr(const shuffle_vector_exprt &value)
const side_effect_expr_overflowt & to_side_effect_expr_overflow(const exprt &expr)
Cast an exprt to a side_effect_expr_overflowt.
bool can_cast_expr< shuffle_vector_exprt >(const exprt &base)
A class for an expression that represents a conditional target or a list of targets sharing a common ...
const exprt::operandst & targets() const
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
const exprt & condition() const
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
exprt::operandst & targets()
conditional_target_group_exprt(exprt _condition, exprt _target_list)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
A class for an expression that indicates a history variable.
const exprt & expression() const
history_exprt(exprt variable, const irep_idt &id)
const irep_idt & id() const
A base class for multi-ary expressions Associativity is not specified.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Shuffle elements of one or two vectors, modelled after Clang's __builtin_shufflevector.
const vector_typet & type() const
const exprt & vector2() const
shuffle_vector_exprt(exprt vector1, optionalt< exprt > vector2, exprt::operandst indices)
const exprt::operandst & indices() const
vector_exprt lower() const
bool has_two_input_vectors() const
exprt::operandst & indices()
const exprt & vector1() const
A Boolean expression returning true, iff the result of performing operation kind on operands a and b ...
const exprt & lhs() const
const exprt & result() const
const exprt & rhs() const
side_effect_expr_overflowt(const irep_idt &kind, exprt _lhs, exprt _rhs, exprt _result, const source_locationt &loc)
An expression containing a side effect.
const irep_idt & get_statement() const
Generic base class for unary expressions.
Vector constructor from list of elements.
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
const std::string & id2string(const irep_idt &d)
nonstd::optional< T > optionalt
#define PRECONDITION(CONDITION)
side_effect_exprt & to_side_effect_expr(exprt &expr)
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...