cprover
cpp_enum_type.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: C++ Language Type Checking
4 
5 Author: Daniel Kroening, kroening@cs.cmu.edu
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_CPP_CPP_ENUM_TYPE_H
13 #define CPROVER_CPP_CPP_ENUM_TYPE_H
14 
15 #include <cassert>
16 
17 #include <util/type.h>
18 
19 #include "cpp_name.h"
20 
21 class cpp_enum_typet:public typet
22 {
23 public:
25 
26  const cpp_namet &tag() const
27  {
28  return static_cast<const cpp_namet &>(find(ID_tag));
29  }
30 
31  bool has_tag() const
32  {
33  return find(ID_tag).is_not_nil();
34  }
35 
37  {
38  return static_cast<cpp_namet &>(add(ID_tag));
39  }
40 
41  const irept &body() const
42  {
43  return find(ID_body);
44  }
45 
47  {
48  return add(ID_body);
49  }
50 
51  bool has_body() const
52  {
53  return find(ID_body).is_not_nil();
54  }
55 
57  {
58  return get_bool(ID_C_tag_only_declaration);
59  }
60 
62 };
63 
64 inline const cpp_enum_typet &to_cpp_enum_type(const irept &irep)
65 {
66  assert(irep.id()==ID_c_enum);
67  return static_cast<const cpp_enum_typet &>(irep);
68 }
69 
71 {
72  assert(irep.id()==ID_c_enum);
73  return static_cast<cpp_enum_typet &>(irep);
74 }
75 
76 #endif // CPROVER_CPP_CPP_ENUM_TYPE_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
cpp_enum_typet::body
irept & body()
Definition: cpp_enum_type.h:46
to_cpp_enum_type
const cpp_enum_typet & to_cpp_enum_type(const irept &irep)
Definition: cpp_enum_type.h:64
typet
The type of an expression, extends irept.
Definition: type.h:29
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
type.h
Defines typet, type_with_subtypet and type_with_subtypest.
cpp_enum_typet::get_tag_only_declaration
bool get_tag_only_declaration() const
Definition: cpp_enum_type.h:56
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
cpp_enum_typet::generate_anon_tag
irep_idt generate_anon_tag() const
Definition: cpp_enum_type.cpp:20
irept::id
const irep_idt & id() const
Definition: irep.h:418
cpp_enum_typet::body
const irept & body() const
Definition: cpp_enum_type.h:41
cpp_enum_typet
Definition: cpp_enum_type.h:22
cpp_enum_typet::has_body
bool has_body() const
Definition: cpp_enum_type.h:51
cpp_enum_typet::tag
cpp_namet & tag()
Definition: cpp_enum_type.h:36
cpp_enum_typet::cpp_enum_typet
cpp_enum_typet()
Definition: cpp_enum_type.cpp:16
cpp_enum_typet::has_tag
bool has_tag() const
Definition: cpp_enum_type.h:31
cpp_enum_typet::tag
const cpp_namet & tag() const
Definition: cpp_enum_type.h:26
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:394
cpp_namet
Definition: cpp_name.h:17
cpp_name.h