CBMC
Loading...
Searching...
No Matches
Classes | Functions
byte_operators.h File Reference

Expression classes for byte-level operators. More...

#include "invariant.h"
#include "std_expr.h"
+ Include dependency graph for byte_operators.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class   byte_extract_exprt
  Expression of type type extracted from some object op starting at position offset (given in number of bytes). More...
 
class   byte_update_exprt
  Expression corresponding to op() where the bytes starting at position offset (given in number of bytes) have been updated with value. More...
 

Functions

template<>
bool  can_cast_expr< byte_extract_exprt > (const exprt &base)
 
const byte_extract_exprt &  to_byte_extract_expr (const exprt &expr)
 
byte_extract_exprt &  to_byte_extract_expr (exprt &expr)
 
void  validate_expr (const byte_extract_exprt &value)
 
template<>
bool  can_cast_expr< byte_update_exprt > (const exprt &base)
 
const byte_update_exprt &  to_byte_update_expr (const exprt &expr)
 
byte_update_exprt &  to_byte_update_expr (exprt &expr)
 
byte_extract_exprt  make_byte_extract (const exprt &_op, const exprt &_offset, const typet &_type)
  Construct a byte_extract_exprt with endianness and byte width matching the current configuration.
 
byte_update_exprt  make_byte_update (const exprt &_op, const exprt &_offset, const exprt &_value)
  Construct a byte_update_exprt with endianness and byte width matching the current configuration.
 
bool  has_byte_operator (const exprt &src)
  Return true iff src or one of its operands contain a byte extract or byte update expression.
 
exprt  lower_byte_extract (const byte_extract_exprt &src, const namespacet &ns)
  Rewrite a byte extract expression to more fundamental operations.
 
exprt  lower_byte_update (const byte_update_exprt &src, const namespacet &ns)
  Rewrite a byte update expression to more fundamental operations.
 
exprt  lower_byte_operators (const exprt &src, const namespacet &ns)
  Rewrite an expression possibly containing byte-extract or -update expressions to more fundamental operations.
 

Detailed Description

Expression classes for byte-level operators.

Author
Daniel Kroening kroen.nosp@m.ing@.nosp@m.kroen.nosp@m.ing..nosp@m.com
Date
Sun Jul 31 21:54:44 BST 2011

Definition in file byte_operators.h.

Function Documentation

◆  can_cast_expr< byte_extract_exprt >()

template<>
bool can_cast_expr< byte_extract_exprt > ( const exprt &  base )
inline

Definition at line 64 of file byte_operators.h.

◆  can_cast_expr< byte_update_exprt >()

template<>
bool can_cast_expr< byte_update_exprt > ( const exprt &  base )
inline

Definition at line 137 of file byte_operators.h.

◆  has_byte_operator()

bool has_byte_operator ( const exprt &  src )

Return true iff src or one of its operands contain a byte extract or byte update expression.

Definition at line 61 of file byte_operators.cpp.

◆  lower_byte_extract()

exprt lower_byte_extract ( const byte_extract_exprt &  src,
const namespacet &  ns 
)

Rewrite a byte extract expression to more fundamental operations.

Parameters
src Byte extract expression
ns Namespace
Returns
Semantically equivalent expression such that the top-level expression no longer is a byte_extract_exprt or byte_update_exprt. Use lower_byte_operators to also remove all byte operators from any operands of src.

Rewrite a byte extract expression to more fundamental operations.

Definition at line 1242 of file lower_byte_operators.cpp.

◆  lower_byte_operators()

exprt lower_byte_operators ( const exprt &  src,
const namespacet &  ns 
)

Rewrite an expression possibly containing byte-extract or -update expressions to more fundamental operations.

Parameters
src Input expression
ns Namespace
Returns
Semantically equivalent expression that does not contain any byte_extract_exprt or byte_update_exprt.

Definition at line 2665 of file lower_byte_operators.cpp.

◆  lower_byte_update()

exprt lower_byte_update ( const byte_update_exprt &  src,
const namespacet &  ns 
)

Rewrite a byte update expression to more fundamental operations.

Parameters
src Byte update expression
ns Namespace
Returns
Semantically equivalent expression such that the top-level expression no longer is a byte_extract_exprt or byte_update_exprt. Use lower_byte_operators to also remove all byte operators from any operands of src.

Definition at line 2572 of file lower_byte_operators.cpp.

◆  make_byte_extract()

byte_extract_exprt make_byte_extract ( const exprt &  _op,
const exprt &  _offset,
const typet &  _type 
)

Construct a byte_extract_exprt with endianness and byte width matching the current configuration.

Definition at line 48 of file byte_operators.cpp.

◆  make_byte_update()

byte_update_exprt make_byte_update ( const exprt &  _op,
const exprt &  _offset,
const exprt &  _value 
)

Construct a byte_update_exprt with endianness and byte width matching the current configuration.

Definition at line 55 of file byte_operators.cpp.

◆  to_byte_extract_expr() [1/2]

const byte_extract_exprt & to_byte_extract_expr ( const exprt &  expr )
inline

Definition at line 70 of file byte_operators.h.

◆  to_byte_extract_expr() [2/2]

byte_extract_exprt & to_byte_extract_expr ( exprt &  expr )
inline

Definition at line 76 of file byte_operators.h.

◆  to_byte_update_expr() [1/2]

const byte_update_exprt & to_byte_update_expr ( const exprt &  expr )
inline

Definition at line 143 of file byte_operators.h.

◆  to_byte_update_expr() [2/2]

byte_update_exprt & to_byte_update_expr ( exprt &  expr )
inline

Definition at line 149 of file byte_operators.h.

◆  validate_expr()

void validate_expr ( const byte_extract_exprt &  value )
inline

Definition at line 82 of file byte_operators.h.

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