CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
cpp_storage_spec.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@cs.cmu.edu
6
7\*******************************************************************/
8
9
10#ifndef CPROVER_CPP_CPP_STORAGE_SPEC_H
11#define CPROVER_CPP_CPP_STORAGE_SPEC_H
12
14
15class typet;
16
18{
19public:
23
24 explicit cpp_storage_spect(const typet &type)
25 {
26 read(type);
27 }
28
30 {
31 return static_cast<source_locationt &>(add(ID_C_source_location));
32 }
33
35 {
36 return static_cast<const source_locationt &>(find(ID_C_source_location));
37 }
38
39 bool is_static() const { return get_bool(ID_static); }
40 bool is_extern() const { return get_bool(ID_extern); }
41 bool is_auto() const { return get_bool(ID_auto); }
42 bool is_register() const { return get_bool(ID_register); }
43 bool is_mutable() const { return get_bool(ID_mutable); }
44 bool is_thread_local() const { return get_bool(ID_thread_local); }
45 bool is_asm() const { return get_bool(ID_asm); }
46 bool is_weak() const
47 {
48 return get_bool(ID_weak);
49 }
50
51 void set_static() { set(ID_static, true); }
52 void set_extern() { set(ID_extern, true); }
53 void set_auto() { set(ID_auto, true); }
54 void set_register() { set(ID_register, true); }
55 void set_mutable() { set(ID_mutable, true); }
57 void set_asm() { set(ID_asm, true); }
58 void set_weak()
59 {
60 set(ID_weak, true);
61 }
62
63 bool is_empty() const
64 {
65 return !is_static() && !is_extern() && !is_auto() && !is_register() &&
66 !is_mutable() && !is_thread_local() && !is_asm() && !is_weak();
67 }
68
70 {
71 if(other.is_static())
72 set_static();
73 if(other.is_extern())
74 set_extern();
75 if(other.is_auto())
76 set_auto();
77 if(other.is_register())
79 if(other.is_mutable())
81 if(other.is_thread_local())
83 if(other.is_asm())
84 set_asm();
85 if(other.is_weak())
86 set_weak();
87
88 return *this;
89 }
90
91private:
92 void read(const typet &type);
93};
94
95#endif // CPROVER_CPP_CPP_STORAGE_SPEC_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
bool is_register() const
cpp_storage_spect(const typet &type)
bool is_static() const
bool is_empty() const
cpp_storage_spect & operator|=(const cpp_storage_spect &other)
source_locationt & location()
bool is_mutable() const
bool is_thread_local() const
bool is_extern() const
const source_locationt & location() const
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:364
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
const irept & find(const irep_idt &name) const
Definition irep.cpp:93
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
irept & add(const irep_idt &name)
Definition irep.cpp:103
The type of an expression, extends irept.
Definition type.h:29