cprover
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/type.h>
14 
16 {
17 public:
18  cpp_storage_spect():irept(ID_cpp_storage_spec)
19  {
20  }
21 
22  explicit cpp_storage_spect(const typet &type)
23  {
24  read(type);
25  }
26 
28  {
29  return static_cast<source_locationt &>(add(ID_C_source_location));
30  }
31 
32  const source_locationt &location() const
33  {
34  return static_cast<const source_locationt &>(find(ID_C_source_location));
35  }
36 
37  bool is_static() const { return get_bool(ID_static); }
38  bool is_extern() const { return get_bool(ID_extern); }
39  bool is_auto() const { return get_bool(ID_auto); }
40  bool is_register() const { return get_bool(ID_register); }
41  bool is_mutable() const { return get_bool(ID_mutable); }
42  bool is_thread_local() const { return get_bool(ID_thread_local); }
43  bool is_asm() const { return get_bool(ID_asm); }
44  bool is_weak() const
45  {
46  return get_bool(ID_weak);
47  }
48 
49  void set_static() { set(ID_static, true); }
50  void set_extern() { set(ID_extern, true); }
51  void set_auto() { set(ID_auto, true); }
52  void set_register() { set(ID_register, true); }
53  void set_mutable() { set(ID_mutable, true); }
54  void set_thread_local() { set(ID_thread_local, true); }
55  void set_asm() { set(ID_asm, true); }
56  void set_weak()
57  {
58  set(ID_weak, true);
59  }
60 
61  bool is_empty() const
62  {
63  return !is_static() && !is_extern() && !is_auto() && !is_register() &&
64  !is_mutable() && !is_thread_local() && !is_asm() && !is_weak();
65  }
66 
68  {
69  if(other.is_static())
70  set_static();
71  if(other.is_extern())
72  set_extern();
73  if(other.is_auto())
74  set_auto();
75  if(other.is_register())
76  set_register();
77  if(other.is_mutable())
78  set_mutable();
79  if(other.is_thread_local())
81  if(other.is_asm())
82  set_asm();
83  if(other.is_weak())
84  set_weak();
85 
86  return *this;
87  }
88 
89 private:
90  void read(const typet &type);
91 };
92 
93 #endif // CPROVER_CPP_CPP_STORAGE_SPEC_H
cpp_storage_spect
Definition: cpp_storage_spec.h:16
cpp_storage_spect::set_mutable
void set_mutable()
Definition: cpp_storage_spec.h:53
typet
The type of an expression, extends irept.
Definition: type.h:29
cpp_storage_spect::is_asm
bool is_asm() const
Definition: cpp_storage_spec.h:43
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:113
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
cpp_storage_spect::set_extern
void set_extern()
Definition: cpp_storage_spec.h:50
cpp_storage_spect::set_static
void set_static()
Definition: cpp_storage_spec.h:49
cpp_storage_spect::is_extern
bool is_extern() const
Definition: cpp_storage_spec.h:38
cpp_storage_spect::is_empty
bool is_empty() const
Definition: cpp_storage_spec.h:61
cpp_storage_spect::operator|=
cpp_storage_spect & operator|=(const cpp_storage_spect &other)
Definition: cpp_storage_spec.h:67
cpp_storage_spect::is_static
bool is_static() const
Definition: cpp_storage_spec.h:37
type.h
Defines typet, type_with_subtypet and type_with_subtypest.
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
sharing_treet< irept, std::map< irep_namet, irept > >::read
const dt & read() const
Definition: irep.h:270
cpp_storage_spect::is_mutable
bool is_mutable() const
Definition: cpp_storage_spec.h:41
cpp_storage_spect::set_register
void set_register()
Definition: cpp_storage_spec.h:52
cpp_storage_spect::cpp_storage_spect
cpp_storage_spect()
Definition: cpp_storage_spec.h:18
cpp_storage_spect::cpp_storage_spect
cpp_storage_spect(const typet &type)
Definition: cpp_storage_spec.h:22
cpp_storage_spect::is_auto
bool is_auto() const
Definition: cpp_storage_spec.h:39
cpp_storage_spect::location
source_locationt & location()
Definition: cpp_storage_spec.h:27
cpp_storage_spect::is_register
bool is_register() const
Definition: cpp_storage_spec.h:40
source_locationt
Definition: source_location.h:20
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
cpp_storage_spect::is_thread_local
bool is_thread_local() const
Definition: cpp_storage_spec.h:42
cpp_storage_spect::set_thread_local
void set_thread_local()
Definition: cpp_storage_spec.h:54
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:394
cpp_storage_spect::set_auto
void set_auto()
Definition: cpp_storage_spec.h:51
cpp_storage_spect::set_asm
void set_asm()
Definition: cpp_storage_spec.h:55
cpp_storage_spect::location
const source_locationt & location() const
Definition: cpp_storage_spec.h:32
cpp_storage_spect::is_weak
bool is_weak() const
Definition: cpp_storage_spec.h:44
cpp_storage_spect::set_weak
void set_weak()
Definition: cpp_storage_spec.h:56