CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
designator.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: ANSI-C Language Type Checking
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_ANSI_C_DESIGNATOR_H
13#define CPROVER_ANSI_C_DESIGNATOR_H
14
15#include <vector>
16#include <iosfwd>
17
18#include <util/type.h>
19
21{
22public:
23 struct entryt
24 {
25 size_t index;
26 size_t size;
29
30 explicit entryt(const typet &type):
32 {
33 }
34 };
35
36 bool empty() const { return index_list.empty(); }
37 size_t size() const { return index_list.size(); }
38 const entryt &operator[](size_t i) const { return index_list[i]; }
39 entryt &operator[](size_t i) { return index_list[i]; }
40 const entryt &back() const { return index_list.back(); }
41 const entryt &front() const { return index_list.front(); }
42
44
45 void push_entry(const entryt &entry)
46 {
47 index_list.push_back(entry);
48 }
49
50 void pop_entry()
51 {
52 index_list.pop_back();
53 }
54
55 void print(std::ostream &out) const;
56
57protected:
58 // a list of indices into arrays or structs
59 typedef std::vector<entryt> index_listt;
61};
62
63inline std::ostream &operator << (std::ostream &os, const designatort &d)
64{
65 d.print(os);
66 return os;
67}
68
69#endif // CPROVER_ANSI_C_DESIGNATOR_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
const entryt & front() const
Definition designator.h:41
const entryt & operator[](size_t i) const
Definition designator.h:38
void print(std::ostream &out) const
entryt & operator[](size_t i)
Definition designator.h:39
index_listt index_list
Definition designator.h:60
size_t size() const
Definition designator.h:37
void push_entry(const entryt &entry)
Definition designator.h:45
const entryt & back() const
Definition designator.h:40
bool empty() const
Definition designator.h:36
void pop_entry()
Definition designator.h:50
std::vector< entryt > index_listt
Definition designator.h:59
The type of an expression, extends irept.
Definition type.h:29
std::ostream & operator<<(std::ostream &os, const designatort &d)
Definition designator.h:63
entryt(const typet &type)
Definition designator.h:30
Defines typet, type_with_subtypet and type_with_subtypest.