cprover
byte_operators.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module:
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
9
#include "
byte_operators.h
"
10
11
#include "
config.h
"
12
13
irep_idt
byte_extract_id
()
14
{
15
switch
(
config
.
ansi_c
.
endianness
)
16
{
17
case
configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN
:
18
return
ID_byte_extract_little_endian;
19
20
case
configt::ansi_ct::endiannesst::IS_BIG_ENDIAN
:
21
return
ID_byte_extract_big_endian;
22
23
case
configt::ansi_ct::endiannesst::NO_ENDIANNESS
:
24
UNREACHABLE
;
25
}
26
27
UNREACHABLE
;
28
}
29
30
irep_idt
byte_update_id
()
31
{
32
switch
(
config
.
ansi_c
.
endianness
)
33
{
34
case
configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN
:
35
return
ID_byte_update_little_endian;
36
37
case
configt::ansi_ct::endiannesst::IS_BIG_ENDIAN
:
38
return
ID_byte_update_big_endian;
39
40
case
configt::ansi_ct::endiannesst::NO_ENDIANNESS
:
41
UNREACHABLE
;
42
}
43
44
UNREACHABLE
;
45
}
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition:
invariant.h:504
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition:
dstring.h:37
configt::ansi_c
struct configt::ansi_ct ansi_c
byte_update_id
irep_idt byte_update_id()
Definition:
byte_operators.cpp:30
configt::ansi_ct::endiannesst::NO_ENDIANNESS
@ NO_ENDIANNESS
byte_extract_id
irep_idt byte_extract_id()
Definition:
byte_operators.cpp:13
configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN
@ IS_LITTLE_ENDIAN
byte_operators.h
Expression classes for byte-level operators.
config
configt config
Definition:
config.cpp:24
configt::ansi_ct::endiannesst::IS_BIG_ENDIAN
@ IS_BIG_ENDIAN
config.h
configt::ansi_ct::endianness
endiannesst endianness
Definition:
config.h:77
util
byte_operators.cpp
Generated by
1.8.20