CBMC
c_expr.h File Reference

API to expression classes that are internal to the C frontend. More...

#include <util/byte_operators.h>
#include <util/std_code.h>
+ Include dependency graph for c_expr.h:
+ This graph shows which files directly or indirectly include this file:

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...
 

Functions

template<>
bool can_cast_expr< shuffle_vector_exprt > (const exprt &base)
 
void validate_expr (const shuffle_vector_exprt &value)
 
const shuffle_vector_exprtto_shuffle_vector_expr (const exprt &expr)
 Cast an exprt to a shuffle_vector_exprt. More...
 
shuffle_vector_exprtto_shuffle_vector_expr (exprt &expr)
 Cast an exprt to a shuffle_vector_exprt. More...
 
template<>
bool can_cast_expr< side_effect_expr_overflowt > (const exprt &base)
 
const side_effect_expr_overflowtto_side_effect_expr_overflow (const exprt &expr)
 Cast an exprt to a side_effect_expr_overflowt. More...
 
side_effect_expr_overflowtto_side_effect_expr_overflow (exprt &expr)
 Cast an exprt to a side_effect_expr_overflowt. More...
 
const history_exprtto_history_expr (const exprt &expr, const irep_idt &id)
 
void validate_expr (const conditional_target_group_exprt &value)
 
template<>
bool can_cast_expr< conditional_target_group_exprt > (const exprt &base)
 
const conditional_target_group_exprtto_conditional_target_group_expr (const exprt &expr)
 Cast an exprt to a conditional_target_group_exprt. More...
 
conditional_target_group_exprtto_conditional_target_group_expr (exprt &expr)
 Cast an exprt to a conditional_target_group_exprt. More...
 
template<>
bool can_cast_expr< enum_is_in_range_exprt > (const exprt &base)
 
void validate_expr (const enum_is_in_range_exprt &expr)
 
const enum_is_in_range_exprtto_enum_is_in_range_expr (const exprt &expr)
 Cast an exprt to an enum_is_in_range_exprt. More...
 
enum_is_in_range_exprtto_enum_is_in_range_expr (exprt &expr)
 Cast an exprt to a side_effect_expr_overflowt. More...
 
template<>
bool can_cast_expr< bit_cast_exprt > (const exprt &base)
 
void validate_expr (const bit_cast_exprt &value)
 
const bit_cast_exprtto_bit_cast_expr (const exprt &expr)
 Cast an exprt to a bit_cast_exprt. More...
 
bit_cast_exprtto_bit_cast_expr (exprt &expr)
 Cast an exprt to a bit_cast_exprt. More...
 

Detailed Description

API to expression classes that are internal to the C frontend.

Definition in file c_expr.h.

Function Documentation

◆ can_cast_expr< bit_cast_exprt >()

template<>
bool can_cast_expr< bit_cast_exprt > ( const exprt base)
inline

Definition at line 388 of file c_expr.h.

◆ can_cast_expr< conditional_target_group_exprt >()

template<>
bool can_cast_expr< conditional_target_group_exprt > ( const exprt base)
inline

Definition at line 294 of file c_expr.h.

◆ can_cast_expr< enum_is_in_range_exprt >()

template<>
bool can_cast_expr< enum_is_in_range_exprt > ( const exprt base)
inline

Definition at line 339 of file c_expr.h.

◆ can_cast_expr< shuffle_vector_exprt >()

template<>
bool can_cast_expr< shuffle_vector_exprt > ( const exprt base)
inline

Definition at line 77 of file c_expr.h.

◆ can_cast_expr< side_effect_expr_overflowt >()

template<>
bool can_cast_expr< side_effect_expr_overflowt > ( const exprt base)
inline

Definition at line 166 of file c_expr.h.

◆ to_bit_cast_expr() [1/2]

const bit_cast_exprt& to_bit_cast_expr ( const exprt expr)
inline

Cast an exprt to a bit_cast_exprt.

expr must be known to be bit_cast_exprt.

Parameters
exprSource expression
Returns
Object of type bit_cast_exprt

Definition at line 404 of file c_expr.h.

◆ to_bit_cast_expr() [2/2]

bit_cast_exprt& to_bit_cast_expr ( exprt expr)
inline

Cast an exprt to a bit_cast_exprt.

expr must be known to be bit_cast_exprt.

Parameters
exprSource expression
Returns
Object of type bit_cast_exprt

Definition at line 413 of file c_expr.h.

◆ to_conditional_target_group_expr() [1/2]

const conditional_target_group_exprt& to_conditional_target_group_expr ( const exprt expr)
inline

Cast an exprt to a conditional_target_group_exprt.

expr must be known to be conditional_target_group_exprt

Parameters
exprSource expression
Returns
Object of type conditional_target_group_exprt

Definition at line 306 of file c_expr.h.

◆ to_conditional_target_group_expr() [2/2]

conditional_target_group_exprt& to_conditional_target_group_expr ( exprt expr)
inline

Cast an exprt to a conditional_target_group_exprt.

expr must be known to be conditional_target_group_exprt

Parameters
exprSource expression
Returns
Object of type conditional_target_group_exprt

Definition at line 316 of file c_expr.h.

◆ to_enum_is_in_range_expr() [1/2]

const enum_is_in_range_exprt& to_enum_is_in_range_expr ( const exprt expr)
inline

Cast an exprt to an enum_is_in_range_exprt.

expr must be known to be enum_is_in_range_exprt.

Parameters
exprSource expression
Returns
Object of type enum_is_in_range_exprt

Definition at line 356 of file c_expr.h.

◆ to_enum_is_in_range_expr() [2/2]

enum_is_in_range_exprt& to_enum_is_in_range_expr ( exprt expr)
inline

Cast an exprt to a side_effect_expr_overflowt.

expr must be known to be side_effect_expr_overflowt.

Parameters
exprSource expression
Returns
Object of type side_effect_expr_overflowt

Definition at line 366 of file c_expr.h.

◆ to_history_expr()

const history_exprt& to_history_expr ( const exprt expr,
const irep_idt id 
)
inline

Definition at line 220 of file c_expr.h.

◆ to_shuffle_vector_expr() [1/2]

const shuffle_vector_exprt& to_shuffle_vector_expr ( const exprt expr)
inline

Cast an exprt to a shuffle_vector_exprt.

expr must be known to be shuffle_vector_exprt.

Parameters
exprSource expression
Returns
Object of type shuffle_vector_exprt

Definition at line 93 of file c_expr.h.

◆ to_shuffle_vector_expr() [2/2]

shuffle_vector_exprt& to_shuffle_vector_expr ( exprt expr)
inline

Cast an exprt to a shuffle_vector_exprt.

expr must be known to be shuffle_vector_exprt.

Parameters
exprSource expression
Returns
Object of type shuffle_vector_exprt

Definition at line 103 of file c_expr.h.

◆ to_side_effect_expr_overflow() [1/2]

const side_effect_expr_overflowt& to_side_effect_expr_overflow ( const exprt expr)
inline

Cast an exprt to a side_effect_expr_overflowt.

expr must be known to be side_effect_expr_overflowt.

Parameters
exprSource expression
Returns
Object of type side_effect_expr_overflowt

Definition at line 183 of file c_expr.h.

◆ to_side_effect_expr_overflow() [2/2]

side_effect_expr_overflowt& to_side_effect_expr_overflow ( exprt expr)
inline

Cast an exprt to a side_effect_expr_overflowt.

expr must be known to be side_effect_expr_overflowt.

Parameters
exprSource expression
Returns
Object of type side_effect_expr_overflowt

Definition at line 194 of file c_expr.h.

◆ validate_expr() [1/4]

void validate_expr ( const bit_cast_exprt value)
inline

Definition at line 393 of file c_expr.h.

◆ validate_expr() [2/4]

void validate_expr ( const conditional_target_group_exprt value)
inline

Definition at line 288 of file c_expr.h.

◆ validate_expr() [3/4]

void validate_expr ( const enum_is_in_range_exprt expr)
inline

Definition at line 344 of file c_expr.h.

◆ validate_expr() [4/4]

void validate_expr ( const shuffle_vector_exprt value)
inline

Definition at line 82 of file c_expr.h.