CBMC
Toggle main menu visibility
Main Page
Related Pages
Namespaces
Namespace List
Namespace Members
All
a
c
d
e
f
g
j
l
m
r
t
w
Functions
a
c
d
f
g
r
t
w
Typedefs
Enumerations
Classes
Class List
Class Hierarchy
Class Members
All
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
x
y
z
~
Functions
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
x
y
z
~
Variables
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
x
y
z
Typedefs
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
Enumerations
a
b
c
d
e
f
g
i
k
l
m
o
p
r
s
t
u
v
w
Enumerator
a
b
c
d
e
f
h
i
k
l
m
n
o
p
q
r
s
t
u
v
Related Symbols
b
c
d
e
g
i
j
m
n
o
s
t
u
v
Files
File List
File Members
All
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
x
y
z
Functions
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
r
s
t
u
v
w
x
y
z
Variables
_
a
b
c
d
e
f
g
i
l
m
n
o
p
r
s
t
u
w
y
Typedefs
_
a
b
c
d
e
f
g
h
i
j
l
m
n
o
p
r
s
t
u
v
w
Enumerations
_
a
b
c
d
f
g
i
l
m
p
r
s
t
u
v
w
Enumerator
_
a
c
d
e
f
g
h
i
l
m
n
o
p
r
s
t
u
v
w
Macros
_
a
b
c
d
e
f
g
h
i
j
l
m
n
o
p
q
r
s
t
u
v
w
x
y
▼
CBMC
►
Documentation
►
Code Contracts in CBMC
►
The CPROVER C++ API
►
Libcprover-rust
►
Symex and GOTO program instructions
Deprecated List
►
Namespaces
►
Classes
▼
Files
►
File List
►
File Members
•
All
Classes
Namespaces
Files
Functions
Variables
Typedefs
Enumerations
Enumerator
Friends
Macros
Modules
Pages
Loading...
Searching...
No Matches
designator.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: ANSI-C Language Type Checking
4
5
Author: 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
20
class
designatort
21
{
22
public
:
23
struct
entryt
24
{
25
size_t
index
;
26
size_t
size
;
27
bool
vla_permitted
;
28
typet
type
,
subtype
;
29
30
explicit
entryt
(
const
typet
&
type
):
31
index
(0),
size
(0),
vla_permitted
(
false
),
type
(
type
)
32
{
33
}
30
explicit
entryt
(
const
typet
&
type
): {
…
}
34
};
23
struct
entryt
{
…
};
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
43
designatort
() { }
44
45
void
push_entry
(
const
entryt
&entry)
46
{
47
index_list
.push_back(entry);
48
}
45
void
push_entry
(
const
entryt
&entry) {
…
}
49
50
void
pop_entry
()
51
{
52
index_list
.pop_back();
53
}
50
void
pop_entry
() {
…
}
54
55
void
print
(std::ostream &out)
const
;
56
57
protected
:
58
// a list of indices into arrays or structs
59
typedef
std::vector<entryt>
index_listt
;
60
index_listt
index_list
;
61
};
20
class
designatort
{
…
};
62
63
inline
std::ostream &
operator <<
(std::ostream &os,
const
designatort
&d)
64
{
65
d.
print
(os);
66
return
os;
67
}
63
inline
std::ostream &
operator <<
(std::ostream &os,
const
designatort
&d) {
…
}
68
69
#endif
// CPROVER_ANSI_C_DESIGNATOR_H
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition
ai.h:562
designatort
Definition
designator.h:21
designatort::front
const entryt & front() const
Definition
designator.h:41
designatort::operator[]
const entryt & operator[](size_t i) const
Definition
designator.h:38
designatort::print
void print(std::ostream &out) const
Definition
designator.cpp:16
designatort::operator[]
entryt & operator[](size_t i)
Definition
designator.h:39
designatort::index_list
index_listt index_list
Definition
designator.h:60
designatort::size
size_t size() const
Definition
designator.h:37
designatort::push_entry
void push_entry(const entryt &entry)
Definition
designator.h:45
designatort::designatort
designatort()
Definition
designator.h:43
designatort::back
const entryt & back() const
Definition
designator.h:40
designatort::empty
bool empty() const
Definition
designator.h:36
designatort::pop_entry
void pop_entry()
Definition
designator.h:50
designatort::index_listt
std::vector< entryt > index_listt
Definition
designator.h:59
typet
The type of an expression, extends irept.
Definition
type.h:29
operator<<
std::ostream & operator<<(std::ostream &os, const designatort &d)
Definition
designator.h:63
designatort::entryt
Definition
designator.h:24
designatort::entryt::index
size_t index
Definition
designator.h:25
designatort::entryt::size
size_t size
Definition
designator.h:26
designatort::entryt::subtype
typet subtype
Definition
designator.h:28
designatort::entryt::type
typet type
Definition
designator.h:28
designatort::entryt::vla_permitted
bool vla_permitted
Definition
designator.h:27
designatort::entryt::entryt
entryt(const typet &type)
Definition
designator.h:30
type.h
Defines typet, type_with_subtypet and type_with_subtypest.
src
ansi-c
designator.h
Generated by
1.9.8