cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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 <
util/type.h
>
16
17
#include "
cpp_name.h
"
18
19
class
cpp_enum_typet
:
public
typet
20
{
21
public
:
22
cpp_enum_typet
();
23
24
const
cpp_namet
&
tag
()
const
25
{
26
return
static_cast<
const
cpp_namet
&
>
(
find
(ID_tag));
27
}
28
29
bool
has_tag
()
const
30
{
31
return
find
(ID_tag).
is_not_nil
();
32
}
33
34
cpp_namet
&
tag
()
35
{
36
return
static_cast<
cpp_namet
&
>
(
add
(ID_tag));
37
}
38
39
const
irept
&
body
()
const
40
{
41
return
find
(ID_body);
42
}
43
44
irept
&
body
()
45
{
46
return
add
(ID_body);
47
}
48
49
bool
has_body
()
const
50
{
51
return
find
(ID_body).
is_not_nil
();
52
}
53
54
bool
get_tag_only_declaration
()
const
55
{
56
return
get_bool
(ID_C_tag_only_declaration);
57
}
58
59
irep_idt
generate_anon_tag
()
const
;
60
};
61
62
inline
const
cpp_enum_typet
&
to_cpp_enum_type
(
const
irept
&irep)
63
{
64
PRECONDITION
(irep.
id
() == ID_c_enum);
65
return
static_cast<
const
cpp_enum_typet
&
>
(irep);
66
}
67
68
inline
cpp_enum_typet
&
to_cpp_enum_type
(
irept
&irep)
69
{
70
PRECONDITION
(irep.
id
() == ID_c_enum);
71
return
static_cast<
cpp_enum_typet
&
>
(irep);
72
}
73
74
#endif
// CPROVER_CPP_CPP_ENUM_TYPE_H
cpp_enum_typet
Definition
cpp_enum_type.h:20
cpp_enum_typet::has_body
bool has_body() const
Definition
cpp_enum_type.h:49
cpp_enum_typet::cpp_enum_typet
cpp_enum_typet()
Definition
cpp_enum_type.cpp:14
cpp_enum_typet::tag
const cpp_namet & tag() const
Definition
cpp_enum_type.h:24
cpp_enum_typet::body
irept & body()
Definition
cpp_enum_type.h:44
cpp_enum_typet::body
const irept & body() const
Definition
cpp_enum_type.h:39
cpp_enum_typet::has_tag
bool has_tag() const
Definition
cpp_enum_type.h:29
cpp_enum_typet::tag
cpp_namet & tag()
Definition
cpp_enum_type.h:34
cpp_enum_typet::generate_anon_tag
irep_idt generate_anon_tag() const
Definition
cpp_enum_type.cpp:18
cpp_enum_typet::get_tag_only_declaration
bool get_tag_only_declaration() const
Definition
cpp_enum_type.h:54
cpp_namet
Definition
cpp_name.h:17
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition
irep.h:364
irept::get_bool
bool get_bool(const irep_idt &name) const
Definition
irep.cpp:57
irept::find
const irept & find(const irep_idt &name) const
Definition
irep.cpp:93
irept::irept
irept(const irep_idt &_id)
Definition
irep.h:377
irept::is_not_nil
bool is_not_nil() const
Definition
irep.h:372
irept::id
const irep_idt & id() const
Definition
irep.h:388
irept::add
irept & add(const irep_idt &name)
Definition
irep.cpp:103
typet::typet
typet()
Definition
type.h:31
to_cpp_enum_type
const cpp_enum_typet & to_cpp_enum_type(const irept &irep)
Definition
cpp_enum_type.h:62
cpp_name.h
PRECONDITION
#define PRECONDITION(CONDITION)
Definition
invariant.h:463
type.h
Defines typet, type_with_subtypet and type_with_subtypest.
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
cpp
cpp_enum_type.h
Generated by
1.17.0