cprover
Loading...
Searching...
No Matches
byte_operators.cpp File Reference
#include "byte_operators.h"
#include "config.h"
Include dependency graph for byte_operators.cpp:

Go to the source code of this file.

Functions

static irep_idt byte_extract_id ()
static irep_idt byte_update_id ()
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.

Function Documentation

◆ byte_extract_id()

irep_idt byte_extract_id ( )
static

Definition at line 13 of file byte_operators.cpp.

◆ byte_update_id()

irep_idt byte_update_id ( )
static

Definition at line 30 of file byte_operators.cpp.

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

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