CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
c_storage_spec.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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
15class typet;
16
18{
19public:
21 {
22 clear();
23 }
24
25 explicit c_storage_spect(const typet &type)
26 {
27 clear();
28 read(type);
29 }
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();
43 section.clear();
44 }
45
48
49 // __attribute__((alias("foo")))
51
52 // GCC asm labels __asm__("foo") - these change the symbol name
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 &&
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 }
70
71 bool operator!=(const c_storage_spect &other) const
72 {
73 return !(*this==other);
74 }
75
77 {
78 is_typedef |=other.is_typedef;
79 is_extern |=other.is_extern;
80 is_static |=other.is_static;
82 is_inline |=other.is_inline;
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 }
95
96 void read(const typet &type);
97};
98
99#endif // CPROVER_ANSI_C_C_STORAGE_SPEC_H
bool operator==(const c_storage_spect &other) const
c_storage_spect & operator|=(const c_storage_spect &other)
bool operator!=(const c_storage_spect &other) const
c_storage_spect(const typet &type)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
bool empty() const
Definition dstring.h:89
void clear()
Definition dstring.h:159
The type of an expression, extends irept.
Definition type.h:29
int __CPROVER_ID java::java io InputStream read
Definition java.io.c:5