cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
endianness_map.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module:
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
9
10
#ifndef CPROVER_UTIL_ENDIANNESS_MAP_H
11
#define CPROVER_UTIL_ENDIANNESS_MAP_H
12
19
20
#include <iosfwd>
21
#include <vector>
22
23
#include "
invariant.h
"
24
25
class
namespacet
;
26
class
typet
;
27
30
class
endianness_mapt
31
{
32
public
:
33
endianness_mapt
(
34
const
typet
&type,
35
bool
little_endian,
36
const
namespacet
&_ns):
ns
(_ns)
37
{
38
build
(type, little_endian);
39
}
40
41
explicit
endianness_mapt
(
const
namespacet
&_ns) :
ns
(_ns)
42
{
43
}
44
45
virtual
~endianness_mapt
() =
default
;
46
47
size_t
map_bit
(
size_t
bit)
const
48
{
49
PRECONDITION
(bit <
map
.size());
50
size_t
result=
map
[bit];
51
DATA_INVARIANT
(result <
map
.size(),
"bit index must be within bounds"
);
52
return
result;
53
}
54
55
size_t
number_of_bits
()
const
56
{
57
return
map
.size();
58
}
59
60
void
build
(
const
typet
&type,
bool
little_endian);
61
62
void
output
(std::ostream &)
const
;
63
64
protected
:
65
const
namespacet
&
ns
;
66
std::vector<size_t>
map
;
// bit-nr to bit-nr
67
68
virtual
void
build_little_endian
(
const
typet
&type);
69
virtual
void
build_big_endian
(
const
typet
&type);
70
};
71
72
inline
std::ostream &
operator<<
(
73
std::ostream &out,
74
const
endianness_mapt
&m)
75
{
76
m.
output
(out);
77
return
out;
78
}
79
80
#endif
// CPROVER_UTIL_ENDIANNESS_MAP_H
endianness_mapt
Maps a big-endian offset to a little-endian offset.
Definition
endianness_map.h:31
endianness_mapt::ns
const namespacet & ns
Definition
endianness_map.h:65
endianness_mapt::~endianness_mapt
virtual ~endianness_mapt()=default
endianness_mapt::build_big_endian
virtual void build_big_endian(const typet &type)
Definition
endianness_map.cpp:52
endianness_mapt::endianness_mapt
endianness_mapt(const typet &type, bool little_endian, const namespacet &_ns)
Definition
endianness_map.h:33
endianness_mapt::build_little_endian
virtual void build_little_endian(const typet &type)
Definition
endianness_map.cpp:38
endianness_mapt::build
void build(const typet &type, bool little_endian)
Definition
endianness_map.cpp:30
endianness_mapt::endianness_mapt
endianness_mapt(const namespacet &_ns)
Definition
endianness_map.h:41
endianness_mapt::map
std::vector< size_t > map
Definition
endianness_map.h:66
endianness_mapt::number_of_bits
size_t number_of_bits() const
Definition
endianness_map.h:55
endianness_mapt::output
void output(std::ostream &) const
Definition
endianness_map.cpp:18
endianness_mapt::map_bit
size_t map_bit(size_t bit) const
Definition
endianness_map.h:47
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition
namespace.h:91
typet
The type of an expression, extends irept.
Definition
type.h:29
operator<<
std::ostream & operator<<(std::ostream &out, const endianness_mapt &m)
Definition
endianness_map.h:72
invariant.h
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition
invariant.h:534
PRECONDITION
#define PRECONDITION(CONDITION)
Definition
invariant.h:463
util
endianness_map.h
Generated by
1.17.0