CBMC
|
API to expression classes that are internal to the C frontend. More...
Go to the source code of this file.
Classes | |
class | shuffle_vector_exprt |
Shuffle elements of one or two vectors, modelled after Clang's __builtin_shufflevector. More... | |
class | side_effect_expr_overflowt |
A Boolean expression returning true, iff the result of performing operation kind on operands a and b in infinite-precision arithmetic cannot be represented in the type of the object that result points to (or the type of result , if it is not a pointer). More... | |
class | history_exprt |
A class for an expression that indicates a history variable. More... | |
class | conditional_target_group_exprt |
A class for an expression that represents a conditional target or a list of targets sharing a common condition in an assigns clause. More... | |
class | enum_is_in_range_exprt |
A Boolean expression returning true, iff the value of an enum-typed symbol equals one of the enum's declared values. More... | |
class | bit_cast_exprt |
Reinterpret the bits of an expression of type S as an expression of type T where S and T have the same size. More... | |
API to expression classes that are internal to the C frontend.
Definition in file c_expr.h.
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Cast an exprt to a bit_cast_exprt.
expr must be known to be bit_cast_exprt.
expr | Source expression |
|
inline |
Cast an exprt to a bit_cast_exprt.
expr must be known to be bit_cast_exprt.
expr | Source expression |
|
inline |
Cast an exprt to a conditional_target_group_exprt.
expr must be known to be conditional_target_group_exprt
expr | Source expression |
|
inline |
Cast an exprt to a conditional_target_group_exprt.
expr must be known to be conditional_target_group_exprt
expr | Source expression |
|
inline |
Cast an exprt to an enum_is_in_range_exprt.
expr must be known to be enum_is_in_range_exprt.
expr | Source expression |
|
inline |
Cast an exprt to a side_effect_expr_overflowt.
expr must be known to be side_effect_expr_overflowt.
expr | Source expression |
|
inline |
|
inline |
Cast an exprt to a shuffle_vector_exprt.
expr must be known to be shuffle_vector_exprt.
expr | Source expression |
|
inline |
Cast an exprt to a shuffle_vector_exprt.
expr must be known to be shuffle_vector_exprt.
expr | Source expression |
|
inline |
Cast an exprt to a side_effect_expr_overflowt.
expr must be known to be side_effect_expr_overflowt.
expr | Source expression |
|
inline |
Cast an exprt to a side_effect_expr_overflowt.
expr must be known to be side_effect_expr_overflowt.
expr | Source expression |
|
inline |
|
inline |
|
inline |
|
inline |