9#ifndef CPROVER_ANSI_C_C_EXPR_H
10#define CPROVER_ANSI_C_C_EXPR_H
249 "conditional target expression must have two operands");
254 "conditional target second operand must be an ID_expression_list "
255 "expression, found " +
332 op().add_source_location().add_pragma(
"disable:enum-range-check");
347 expr, 1,
"enum_is_in_range expression must have one operand");
Expression classes for byte-level operators.
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 enum_is_in_range_exprt & to_enum_is_in_range_expr(const exprt &expr)
Cast an exprt to an enum_is_in_range_exprt.
const bit_cast_exprt & to_bit_cast_expr(const exprt &expr)
Cast an exprt to a bit_cast_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)
bool can_cast_expr< enum_is_in_range_exprt >(const exprt &base)
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< bit_cast_exprt >(const exprt &base)
bool can_cast_expr< shuffle_vector_exprt >(const exprt &base)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Reinterpret the bits of an expression of type S as an expression of type T where S and T have the sam...
bit_cast_exprt(exprt expr, typet type)
byte_extract_exprt lower() const
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.
A Boolean expression returning true, iff the value of an enum-typed symbol equals one of the enum's d...
exprt lower(const namespacet &ns) const
enum_is_in_range_exprt(exprt _op)
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
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
The type of an expression, extends irept.
Generic base class for unary expressions.
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
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)
#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,...