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
The type of an expression, extends irept.
Definition: type.h:27
Maps a big-endian offset to a little-endian offset.
void build(const typet &type, bool little_endian)
std::ostream & operator<<(std::ostream &out, const endianness_mapt &m)
void output(std::ostream &) const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
endianness_mapt(const namespacet &_ns)
virtual void build_big_endian(const typet &type)
endianness_mapt(const typet &type, bool little_endian, const namespacet &_ns)
size_t number_of_bits() const
std::vector< size_t > map
const namespacet & ns
size_t map_bit(size_t bit) const
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
Definition: invariant.h:485
virtual void build_little_endian(const typet &type)
virtual ~endianness_mapt()=default