cprover
c_expr.h File Reference

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

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

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

Detailed Description

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

Definition in file c_expr.h.

Function Documentation

◆ can_cast_expr< shuffle_vector_exprt >()

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

Definition at line 76 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 165 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 92 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 102 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 182 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 193 of file c_expr.h.

◆ validate_expr()

void validate_expr ( const shuffle_vector_exprt value)
inline

Definition at line 81 of file c_expr.h.