cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
validate_types.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Validate types
4
5
Author: Daniel Poetzl
6
7
\*******************************************************************/
8
9
#include "
validate_types.h
"
10
11
#ifdef REPORT_UNIMPLEMENTED_TYPE_CHECKS
12
#include <iostream>
13
#endif
14
15
#include "
bitvector_types.h
"
// IWYU pragma: keep
16
#include "
c_types.h
"
// IWYU pragma: keep
17
#include "
validate_helpers.h
"
18
19
#define CALL_ON_TYPE(type_type) \
20
C<typet, type_type>()(type, std::forward<Args>(args)...)
21
22
template
<
template
<
typename
,
typename
>
class
C,
typename
... Args>
23
void
call_on_type
(
const
typet
&type, Args &&... args)
24
{
25
if
(type.
id
() == ID_bv)
26
{
27
CALL_ON_TYPE
(
bv_typet
);
28
}
29
else
if
(type.
id
() == ID_unsignedbv)
30
{
31
CALL_ON_TYPE
(
unsignedbv_typet
);
32
}
33
else
if
(type.
id
() == ID_signedbv)
34
{
35
CALL_ON_TYPE
(
signedbv_typet
);
36
}
37
else
if
(type.
id
() == ID_fixedbv)
38
{
39
CALL_ON_TYPE
(
fixedbv_typet
);
40
}
41
else
if
(type.
id
() == ID_floatbv)
42
{
43
CALL_ON_TYPE
(
floatbv_typet
);
44
}
45
else
if
(type.
id
() == ID_pointer)
46
{
47
if
(type.
get_bool
(ID_C_reference))
48
CALL_ON_TYPE
(
reference_typet
);
49
else
50
CALL_ON_TYPE
(
pointer_typet
);
51
}
52
else
if
(type.
id
() == ID_c_bool)
53
{
54
CALL_ON_TYPE
(
c_bool_typet
);
55
}
56
else
if
(type.
id
() == ID_array)
57
{
58
CALL_ON_TYPE
(
array_typet
);
59
}
60
else
61
{
62
#ifdef REPORT_UNIMPLEMENTED_TYPE_CHECKS
63
std::cerr <<
"Unimplemented well-formedness check for type with id: "
64
<< type.
id_string
() << std::endl;
65
#endif
66
67
CALL_ON_TYPE
(
typet
);
68
}
69
}
70
79
void
check_type
(
const
typet
&type,
const
validation_modet
vm)
80
{
81
call_on_type<call_checkt>
(type, vm);
82
}
83
92
void
validate_type
(
93
const
typet
&type,
94
const
namespacet
&ns,
95
const
validation_modet
vm)
96
{
97
call_on_type<call_validatet>
(type, ns, vm);
98
}
99
108
void
validate_full_type
(
109
const
typet
&type,
110
const
namespacet
&ns,
111
const
validation_modet
vm)
112
{
113
call_on_type<call_validate_fullt>
(type, ns, vm);
114
}
bitvector_types.h
Pre-defined bitvector types.
c_types.h
array_typet
Arrays with given size.
Definition
std_types.h:807
bv_typet
Fixed-width bit-vector without numerical interpretation.
Definition
bitvector_types.h:49
c_bool_typet
The C/C++ Booleans.
Definition
c_types.h:97
fixedbv_typet
Fixed-width bit-vector with signed fixed-point interpretation.
Definition
bitvector_types.h:280
floatbv_typet
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition
bitvector_types.h:341
irept::get_bool
bool get_bool(const irep_idt &name) const
Definition
irep.cpp:57
irept::id_string
const std::string & id_string() const
Definition
irep.h:391
irept::id
const irep_idt & id() const
Definition
irep.h:388
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition
namespace.h:91
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition
pointer_expr.h:24
reference_typet
The reference type.
Definition
pointer_expr.h:121
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition
bitvector_types.h:222
typet
The type of an expression, extends irept.
Definition
type.h:29
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition
bitvector_types.h:168
validate_helpers.h
check_type
void check_type(const typet &type, const validation_modet vm)
Check that the given type is well-formed (shallow checks only, i.e., subtypes are not checked).
Definition
validate_types.cpp:79
CALL_ON_TYPE
#define CALL_ON_TYPE(type_type)
Definition
validate_types.cpp:19
validate_type
void validate_type(const typet &type, const namespacet &ns, const validation_modet vm)
Check that the given type is well-formed, assuming that its subtypes have already been checked for we...
Definition
validate_types.cpp:92
call_on_type
void call_on_type(const typet &type, Args &&... args)
Definition
validate_types.cpp:23
validate_full_type
void validate_full_type(const typet &type, const namespacet &ns, const validation_modet vm)
Check that the given type is well-formed (full check, including checks of subtypes).
Definition
validate_types.cpp:108
validate_types.h
validation_modet
validation_modet
Definition
validation_mode.h:13
util
validate_types.cpp
Generated by
1.17.0