CBMC
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{
50 return byte_extract_exprt{
51 byte_extract_id(), _op, _offset, config.ansi_c.char_width, _type};
52}
53
55make_byte_update(const exprt &_op, const exprt &_offset, const exprt &_value)
56{
57 return byte_update_exprt{
58 byte_update_id(), _op, _offset, _value, config.ansi_c.char_width};
59}
60
61bool has_byte_operator(const exprt &src)
62{
63 if(
68 {
69 return true;
70 }
71
72 for(const auto &op : src.operands())
73 {
74 if(has_byte_operator(op))
75 return true;
76 }
77
78 return false;
79}
configt config
Definition config.cpp:25
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()
bool has_byte_operator(const exprt &src)
Return true iff src or one of its operands contain a byte extract or byte update expression.
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.
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:562
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:38
Base class for all expressions.
Definition expr.h:56
operandst & operands()
Definition expr.h:94
const irep_idt & id() const
Definition irep.h:388
The type of an expression, extends irept.
Definition type.h:29
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525