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
•
All
Classes
Namespaces
Files
Functions
Variables
Typedefs
Enumerations
Enumerator
Friends
Macros
Modules
Pages
Loading...
Searching...
No Matches
c_storage_spec.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_ANSI_C_C_STORAGE_SPEC_H
11
#define CPROVER_ANSI_C_C_STORAGE_SPEC_H
12
13
#include <
util/irep.h
>
14
15
class
typet
;
16
17
class
c_storage_spect
18
{
19
public
:
20
c_storage_spect
()
21
{
22
clear
();
23
}
20
c_storage_spect
() {
…
}
24
25
explicit
c_storage_spect
(
const
typet
&type)
26
{
27
clear
();
28
read
(type);
29
}
25
explicit
c_storage_spect
(
const
typet
&type) {
…
}
30
31
void
clear
()
32
{
33
is_typedef
=
false
;
34
is_extern
=
false
;
35
is_thread_local
=
false
;
36
is_static
=
false
;
37
is_register
=
false
;
38
is_inline
=
false
;
39
is_weak
=
false
;
40
is_used
=
false
;
41
alias
.
clear
();
42
asm_label
.
clear
();
43
section
.
clear
();
44
}
31
void
clear
() {
…
}
45
46
bool
is_typedef
,
is_extern
,
is_static
,
is_register
,
47
is_inline
,
is_thread_local
,
is_weak
,
is_used
;
48
49
// __attribute__((alias("foo")))
50
irep_idt
alias
;
51
52
// GCC asm labels __asm__("foo") - these change the symbol name
53
irep_idt
asm_label
;
54
irep_idt
section
;
55
56
bool
operator==
(
const
c_storage_spect
&other)
const
57
{
58
return
is_typedef
==other.
is_typedef
&&
59
is_extern
==other.
is_extern
&&
60
is_static
==other.
is_static
&&
61
is_register
==other.
is_register
&&
62
is_thread_local
==other.
is_thread_local
&&
63
is_inline
==other.
is_inline
&&
64
is_weak
==other.
is_weak
&&
65
is_used
== other.
is_used
&&
66
alias
==other.
alias
&&
67
asm_label
==other.
asm_label
&&
68
section
==other.
section
;
69
}
56
bool
operator==
(
const
c_storage_spect
&other)
const
{
…
}
70
71
bool
operator!=
(
const
c_storage_spect
&other)
const
72
{
73
return
!(*
this
==other);
74
}
71
bool
operator!=
(
const
c_storage_spect
&other)
const
{
…
}
75
76
c_storage_spect
&
operator|=
(
const
c_storage_spect
&other)
77
{
78
is_typedef
|=other.
is_typedef
;
79
is_extern
|=other.
is_extern
;
80
is_static
|=other.
is_static
;
81
is_register
|=other.
is_register
;
82
is_inline
|=other.
is_inline
;
83
is_thread_local
|=other.
is_thread_local
;
84
is_weak
|=other.
is_weak
;
85
is_used
|=other.
is_used
;
86
if
(
alias
.
empty
())
87
alias
=other.
alias
;
88
if
(
asm_label
.
empty
())
89
asm_label
=other.
asm_label
;
90
if
(
section
.
empty
())
91
section
=other.
section
;
92
93
return
*
this
;
94
}
76
c_storage_spect
&
operator|=
(
const
c_storage_spect
&other) {
…
}
95
96
void
read
(
const
typet
&type);
97
};
17
class
c_storage_spect
{
…
};
98
99
#endif
// CPROVER_ANSI_C_C_STORAGE_SPEC_H
c_storage_spect
Definition
c_storage_spec.h:18
c_storage_spect::is_inline
bool is_inline
Definition
c_storage_spec.h:47
c_storage_spect::operator==
bool operator==(const c_storage_spect &other) const
Definition
c_storage_spec.h:56
c_storage_spect::is_weak
bool is_weak
Definition
c_storage_spec.h:47
c_storage_spect::c_storage_spect
c_storage_spect()
Definition
c_storage_spec.h:20
c_storage_spect::is_extern
bool is_extern
Definition
c_storage_spec.h:46
c_storage_spect::is_typedef
bool is_typedef
Definition
c_storage_spec.h:46
c_storage_spect::operator|=
c_storage_spect & operator|=(const c_storage_spect &other)
Definition
c_storage_spec.h:76
c_storage_spect::alias
irep_idt alias
Definition
c_storage_spec.h:50
c_storage_spect::is_used
bool is_used
Definition
c_storage_spec.h:47
c_storage_spect::operator!=
bool operator!=(const c_storage_spect &other) const
Definition
c_storage_spec.h:71
c_storage_spect::section
irep_idt section
Definition
c_storage_spec.h:54
c_storage_spect::asm_label
irep_idt asm_label
Definition
c_storage_spec.h:53
c_storage_spect::is_static
bool is_static
Definition
c_storage_spec.h:46
c_storage_spect::clear
void clear()
Definition
c_storage_spec.h:31
c_storage_spect::is_thread_local
bool is_thread_local
Definition
c_storage_spec.h:47
c_storage_spect::c_storage_spect
c_storage_spect(const typet &type)
Definition
c_storage_spec.h:25
c_storage_spect::is_register
bool is_register
Definition
c_storage_spec.h:46
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition
dstring.h:38
dstringt::empty
bool empty() const
Definition
dstring.h:89
dstringt::clear
void clear()
Definition
dstring.h:159
typet
The type of an expression, extends irept.
Definition
type.h:29
irep.h
read
int __CPROVER_ID java::java io InputStream read
Definition
java.io.c:5
src
ansi-c
c_storage_spec.h
Generated by
1.9.8