CBMC
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 <iosfwd>
21 #include <vector>
22 
23 #include "invariant.h"
24 
25 class namespacet;
26 class typet;
27 
31 {
32 public:
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
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:94
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