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

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 51 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 111 of file byte_operators.h.

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 54 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 57 of file byte_operators.h.

to_byte_extract_expr() [2/2]

byte_extract_exprt& to_byte_extract_expr ( exprt &  expr )

inline

Definition at line 63 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 117 of file byte_operators.h.

to_byte_update_expr() [2/2]

byte_update_exprt& to_byte_update_expr ( exprt &  expr )

inline

Definition at line 123 of file byte_operators.h.

validate_expr()

void validate_expr ( const byte_extract_exprt &  value )

inline

Definition at line 69 of file byte_operators.h.