CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
typedef_type.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#ifndef CPROVER_ANSI_C_TYPEDEF_TYPE_H
10#define CPROVER_ANSI_C_TYPEDEF_TYPE_H
11
12#include <util/type.h>
13
15class typedef_typet : public typet
16{
17public:
18 explicit typedef_typet(const irep_idt &identifier) : typet(ID_typedef_type)
19 {
20 set_identifier(identifier);
21 }
22
23 void set_identifier(const irep_idt &identifier)
24 {
25 set(ID_identifier, identifier);
26 }
27
28 const irep_idt &get_identifier() const
29 {
30 return get(ID_identifier);
31 }
32};
33
39inline const typedef_typet &to_typedef_type(const typet &type)
40{
42 return static_cast<const typedef_typet &>(type);
43}
44
48{
50 return static_cast<typedef_typet &>(type);
51}
52
53template <>
54inline bool can_cast_type<typedef_typet>(const typet &type)
55{
56 return type.id() == ID_typedef_type;
57}
58
59#endif // CPROVER_ANSI_C_TYPEDEF_TYPE_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
const irep_idt & id() const
Definition irep.h:388
A typedef.
typedef_typet(const irep_idt &identifier)
void set_identifier(const irep_idt &identifier)
const irep_idt & get_identifier() const
The type of an expression, extends irept.
Definition type.h:29
#define PRECONDITION(CONDITION)
Definition invariant.h:463
Defines typet, type_with_subtypet and type_with_subtypest.
bool can_cast_type< typedef_typet >(const typet &type)
const typedef_typet & to_typedef_type(const typet &type)
Cast a generic typet to a typedef_typet.