cprover
Loading...
Searching...
No Matches
byte_operators.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "byte_operators.h"
10
11#include "config.h"
12
29
46
48make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
49{
51}
52
54make_byte_update(const exprt &_op, const exprt &_offset, const exprt &_value)
55{
56 return byte_update_exprt{byte_update_id(), _op, _offset, _value};
57}
Expression classes for byte-level operators.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Expression of type type extracted from some object op starting at position offset (given in number of...
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Base class for all expressions.
Definition expr.h:54
The type of an expression, extends irept.
Definition type.h:29
configt config
Definition config.cpp:25
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:503
static irep_idt byte_extract_id()
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.
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.