-
Notifications
You must be signed in to change notification settings - Fork 300
Expand file tree
/
Copy pathbyte_operators.cpp
More file actions
79 lines (61 loc) · 1.7 KB
/
Copy pathbyte_operators.cpp
File metadata and controls
79 lines (61 loc) · 1.7 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
/*******************************************************************\
Module:
Author: Daniel Kroening, kroening@kroening.com
\*******************************************************************/
#include "byte_operators.h"
#include "config.h"
static irep_idt byte_extract_id()
{
switch(config.ansi_c.endianness)
{
case configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN:
return ID_byte_extract_little_endian;
case configt::ansi_ct::endiannesst::IS_BIG_ENDIAN:
return ID_byte_extract_big_endian;
case configt::ansi_ct::endiannesst::NO_ENDIANNESS:
UNREACHABLE;
}
UNREACHABLE;
}
static irep_idt byte_update_id()
{
switch(config.ansi_c.endianness)
{
case configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN:
return ID_byte_update_little_endian;
case configt::ansi_ct::endiannesst::IS_BIG_ENDIAN:
return ID_byte_update_big_endian;
case configt::ansi_ct::endiannesst::NO_ENDIANNESS:
UNREACHABLE;
}
UNREACHABLE;
}
byte_extract_exprt
make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
{
return byte_extract_exprt{
byte_extract_id(), _op, _offset, config.ansi_c.char_width, _type};
}
byte_update_exprt
make_byte_update(const exprt &_op, const exprt &_offset, const exprt &_value)
{
return byte_update_exprt{
byte_update_id(), _op, _offset, _value, config.ansi_c.char_width};
}
bool has_byte_operator(const exprt &src)
{
if(
src.id() == ID_byte_update_little_endian ||
src.id() == ID_byte_update_big_endian ||
src.id() == ID_byte_extract_little_endian ||
src.id() == ID_byte_extract_big_endian)
{
return true;
}
for(const auto &op : src.operands())
{
if(has_byte_operator(op))
return true;
}
return false;
}