-
Notifications
You must be signed in to change notification settings - Fork 289
Expand file tree
/
Copy pathcpp_template_type.h
More file actions
78 lines (58 loc) · 1.65 KB
/
cpp_template_type.h
File metadata and controls
78 lines (58 loc) · 1.65 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
/*******************************************************************\
Module:
Author: Daniel Kroening, [email protected]
\*******************************************************************/
#ifndef CPROVER_CPP_CPP_TEMPLATE_TYPE_H
#define CPROVER_CPP_CPP_TEMPLATE_TYPE_H
#include <util/invariant.h>
#include <util/type.h>
#include "cpp_template_parameter.h"
class template_typet:public typet
{
public:
template_typet():typet(ID_template)
{
}
typedef std::vector<template_parametert> template_parameterst;
template_parameterst &template_parameters()
{
return (template_parameterst &)add(ID_template_parameters).get_sub();
}
const template_parameterst &template_parameters() const
{
return (const template_parameterst &)find(ID_template_parameters).get_sub();
}
const typet &subtype() const
{
if(get_sub().empty())
return static_cast<const typet &>(get_nil_irep());
return static_cast<const typet &>(get_sub().front());
}
typet &subtype()
{
return add_subtype();
}
};
inline template_typet &to_template_type(typet &type)
{
PRECONDITION(type.id() == ID_template);
return static_cast<template_typet &>(type);
}
inline const template_typet &to_template_type(const typet &type)
{
PRECONDITION(type.id() == ID_template);
return static_cast<const template_typet &>(type);
}
inline const typet &template_subtype(const typet &type)
{
if(type.id()==ID_template)
return to_type_with_subtype(type).subtype();
return type;
}
inline typet &template_subtype(typet &type)
{
if(type.id()==ID_template)
return to_template_type(type).subtype();
return type;
}
#endif // CPROVER_CPP_CPP_TEMPLATE_TYPE_H