CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
endianness_map.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9
10#ifndef CPROVER_UTIL_ENDIANNESS_MAP_H
11#define CPROVER_UTIL_ENDIANNESS_MAP_H
12
20#include <iosfwd>
21#include <vector>
22
23#include "invariant.h"
24
25class namespacet;
26class typet;
27
31{
32public:
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
64protected:
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
72inline 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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Maps a big-endian offset to a little-endian offset.
const namespacet & ns
virtual ~endianness_mapt()=default
virtual void build_big_endian(const typet &type)
endianness_mapt(const typet &type, bool little_endian, const namespacet &_ns)
virtual void build_little_endian(const typet &type)
void build(const typet &type, bool little_endian)
endianness_mapt(const namespacet &_ns)
std::vector< size_t > map
size_t number_of_bits() const
void output(std::ostream &) const
size_t map_bit(size_t bit) const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The type of an expression, extends irept.
Definition type.h:29
std::ostream & operator<<(std::ostream &out, const endianness_mapt &m)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463