CBMC
cpp_storage_spec.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: 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 
13 #include <util/source_location.h>
14 
15 class typet;
16 
18 {
19 public:
20  cpp_storage_spect():irept(ID_cpp_storage_spec)
21  {
22  }
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 
34  const source_locationt &location() const
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); }
56  void set_thread_local() { set(ID_thread_local, 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())
78  set_register();
79  if(other.is_mutable())
80  set_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 
91 private:
92  void read(const typet &type);
93 };
94 
95 #endif // CPROVER_CPP_CPP_STORAGE_SPEC_H
cpp_storage_spect & operator|=(const cpp_storage_spect &other)
source_locationt & location()
bool is_register() const
cpp_storage_spect(const typet &type)
bool is_static() const
bool is_empty() const
bool is_auto() const
bool is_mutable() const
bool is_thread_local() const
bool is_extern() const
const source_locationt & location() const
bool is_asm() const
bool is_weak() const
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:360
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:408
irept & add(const irep_idt &name)
Definition: irep.cpp:103
The type of an expression, extends irept.
Definition: type.h:29