cprover
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 
20 #include <cassert>
21 #include <iosfwd>
22 #include <vector>
23 
24 #include "invariant.h"
25 
26 class namespacet;
27 class typet;
28 
32 {
33 public:
35  const typet &type,
36  bool little_endian,
37  const namespacet &_ns):ns(_ns)
38  {
39  build(type, little_endian);
40  }
41 
42  explicit endianness_mapt(const namespacet &_ns) : ns(_ns)
43  {
44  }
45 
46  virtual ~endianness_mapt() = default;
47 
48  size_t map_bit(size_t bit) const
49  {
50  PRECONDITION(bit < map.size());
51  size_t result=map[bit];
52  DATA_INVARIANT(result < map.size(), "bit index must be within bounds");
53  return result;
54  }
55 
56  size_t number_of_bits() const
57  {
58  return map.size();
59  }
60 
61  void build(const typet &type, bool little_endian);
62 
63  void output(std::ostream &) const;
64 
65 protected:
66  const namespacet &ns;
67  std::vector<size_t> map; // bit-nr to bit-nr
68 
69  virtual void build_little_endian(const typet &type);
70  virtual void build_big_endian(const typet &type);
71 };
72 
73 inline std::ostream &operator<<(
74  std::ostream &out,
75  const endianness_mapt &m)
76 {
77  m.output(out);
78  return out;
79 }
80 
81 #endif // CPROVER_UTIL_ENDIANNESS_MAP_H
endianness_mapt::build
void build(const typet &type, bool little_endian)
Definition: endianness_map.cpp:30
typet
The type of an expression, extends irept.
Definition: type.h:29
endianness_mapt::endianness_mapt
endianness_mapt(const namespacet &_ns)
Definition: endianness_map.h:42
operator<<
std::ostream & operator<<(std::ostream &out, const endianness_mapt &m)
Definition: endianness_map.h:73
endianness_mapt::build_little_endian
virtual void build_little_endian(const typet &type)
Definition: endianness_map.cpp:38
endianness_mapt::endianness_mapt
endianness_mapt(const typet &type, bool little_endian, const namespacet &_ns)
Definition: endianness_map.h:34
endianness_mapt::build_big_endian
virtual void build_big_endian(const typet &type)
Definition: endianness_map.cpp:52
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
endianness_mapt::number_of_bits
size_t number_of_bits() const
Definition: endianness_map.h:56
endianness_mapt::map
std::vector< size_t > map
Definition: endianness_map.h:67
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:511
endianness_mapt::ns
const namespacet & ns
Definition: endianness_map.h:66
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
endianness_mapt::map_bit
size_t map_bit(size_t bit) const
Definition: endianness_map.h:48
endianness_mapt::output
void output(std::ostream &) const
Definition: endianness_map.cpp:18
endianness_mapt::~endianness_mapt
virtual ~endianness_mapt()=default
invariant.h
endianness_mapt
Maps a big-endian offset to a little-endian offset.
Definition: endianness_map.h:32