CBMC
Loading...
Searching...
No Matches
Classes | Functions
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_exprt &  to_shuffle_vector_expr (const exprt &expr)
  Cast an exprt to a shuffle_vector_exprt.
 
shuffle_vector_exprt &  to_shuffle_vector_expr (exprt &expr)
  Cast an exprt to a shuffle_vector_exprt.
 
template<>
bool  can_cast_expr< side_effect_expr_overflowt > (const exprt &base)
 
const side_effect_expr_overflowt &  to_side_effect_expr_overflow (const exprt &expr)
  Cast an exprt to a side_effect_expr_overflowt.
 
side_effect_expr_overflowt &  to_side_effect_expr_overflow (exprt &expr)
  Cast an exprt to a side_effect_expr_overflowt.
 
const history_exprt &  to_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_exprt &  to_conditional_target_group_expr (const exprt &expr)
  Cast an exprt to a conditional_target_group_exprt.
 
conditional_target_group_exprt &  to_conditional_target_group_expr (exprt &expr)
  Cast an exprt to a conditional_target_group_exprt.
 
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_exprt &  to_enum_is_in_range_expr (const exprt &expr)
  Cast an exprt to an enum_is_in_range_exprt.
 
enum_is_in_range_exprt &  to_enum_is_in_range_expr (exprt &expr)
  Cast an exprt to a side_effect_expr_overflowt.
 
template<>
bool  can_cast_expr< bit_cast_exprt > (const exprt &base)
 
void  validate_expr (const bit_cast_exprt &value)
 
const bit_cast_exprt &  to_bit_cast_expr (const exprt &expr)
  Cast an exprt to a bit_cast_exprt.
 
bit_cast_exprt &  to_bit_cast_expr (exprt &expr)
  Cast an exprt to a bit_cast_exprt.
 

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

AltStyle によって変換されたページ (->オリジナル) /