cprover
byte_operators.h File Reference

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

#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
 TO_BE_DOCUMENTED. More...
 
class  byte_extract_little_endian_exprt
 TO_BE_DOCUMENTED. More...
 
class  byte_extract_big_endian_exprt
 TO_BE_DOCUMENTED. More...
 
class  byte_update_exprt
 TO_BE_DOCUMENTED. More...
 
class  byte_update_little_endian_exprt
 TO_BE_DOCUMENTED. More...
 
class  byte_update_big_endian_exprt
 TO_BE_DOCUMENTED. More...
 

Functions

const byte_extract_exprtto_byte_extract_expr (const exprt &expr)
 
byte_extract_exprtto_byte_extract_expr (exprt &expr)
 
irep_idt byte_extract_id ()
 
irep_idt byte_update_id ()
 
const byte_extract_little_endian_exprtto_byte_extract_little_endian_expr (const exprt &expr)
 
byte_extract_little_endian_exprtto_byte_extract_little_endian_expr (exprt &expr)
 
const byte_extract_big_endian_exprtto_byte_extract_big_endian_expr (const exprt &expr)
 
byte_extract_big_endian_exprtto_byte_extract_big_endian_expr (exprt &expr)
 
const byte_update_exprtto_byte_update_expr (const exprt &expr)
 
byte_update_exprtto_byte_update_expr (exprt &expr)
 
const byte_update_little_endian_exprtto_byte_update_little_endian_expr (const exprt &expr)
 
byte_update_little_endian_exprtto_byte_update_little_endian_expr (exprt &expr)
 
const byte_update_big_endian_exprtto_byte_update_big_endian_expr (const exprt &expr)
 
byte_update_big_endian_exprtto_byte_update_big_endian_expr (exprt &expr)
 

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

◆ byte_extract_id()

◆ byte_update_id()

◆ to_byte_extract_big_endian_expr() [1/2]

const byte_extract_big_endian_exprt& to_byte_extract_big_endian_expr ( const exprt expr)
inline

Definition at line 110 of file byte_operators.h.

References irept::id(), and exprt::operands().

◆ to_byte_extract_big_endian_expr() [2/2]

byte_extract_big_endian_exprt& to_byte_extract_big_endian_expr ( exprt expr)
inline

Definition at line 117 of file byte_operators.h.

References irept::id(), and exprt::operands().

◆ to_byte_extract_expr() [1/2]

◆ to_byte_extract_expr() [2/2]

byte_extract_exprt& to_byte_extract_expr ( exprt expr)
inline

Definition at line 58 of file byte_operators.h.

References exprt::operands().

◆ to_byte_extract_little_endian_expr() [1/2]

const byte_extract_little_endian_exprt& to_byte_extract_little_endian_expr ( const exprt expr)
inline

Definition at line 79 of file byte_operators.h.

References irept::id(), and exprt::operands().

◆ to_byte_extract_little_endian_expr() [2/2]

byte_extract_little_endian_exprt& to_byte_extract_little_endian_expr ( exprt expr)
inline

Definition at line 86 of file byte_operators.h.

References irept::id(), and exprt::operands().

◆ to_byte_update_big_endian_expr() [1/2]

const byte_update_big_endian_exprt& to_byte_update_big_endian_expr ( const exprt expr)
inline

Definition at line 217 of file byte_operators.h.

References irept::id(), and exprt::operands().

◆ to_byte_update_big_endian_expr() [2/2]

byte_update_big_endian_exprt& to_byte_update_big_endian_expr ( exprt expr)
inline

Definition at line 224 of file byte_operators.h.

References irept::id(), and exprt::operands().

◆ to_byte_update_expr() [1/2]

const byte_update_exprt& to_byte_update_expr ( const exprt expr)
inline

◆ to_byte_update_expr() [2/2]

byte_update_exprt& to_byte_update_expr ( exprt expr)
inline

Definition at line 162 of file byte_operators.h.

References exprt::operands().

◆ to_byte_update_little_endian_expr() [1/2]

const byte_update_little_endian_exprt& to_byte_update_little_endian_expr ( const exprt expr)
inline

Definition at line 186 of file byte_operators.h.

References irept::id(), and exprt::operands().

◆ to_byte_update_little_endian_expr() [2/2]

byte_update_little_endian_exprt& to_byte_update_little_endian_expr ( exprt expr)
inline

Definition at line 193 of file byte_operators.h.

References irept::id(), and exprt::operands().