cprover
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 "namespace.h"
16 #include "std_types.h"
17 #include "type.h"
18 #include "validate.h"
19 #include "validate_helpers.h"
20 
21 #define CALL_ON_TYPE(type_type) \
22  C<typet, type_type>()(type, std::forward<Args>(args)...)
23 
24 template <template <typename, typename> class C, typename... Args>
25 void call_on_type(const typet &type, Args &&... args)
26 {
27  if(type.id() == ID_bv)
28  {
30  }
31  else if(type.id() == ID_unsignedbv)
32  {
34  }
35  else if(type.id() == ID_signedbv)
36  {
38  }
39  else if(type.id() == ID_fixedbv)
40  {
42  }
43  else if(type.id() == ID_floatbv)
44  {
46  }
47  else if(type.id() == ID_pointer)
48  {
49  if(type.get_bool(ID_C_reference))
51  else
53  }
54  else if(type.id() == ID_c_bool)
55  {
57  }
58  else if(type.id() == ID_array)
59  {
61  }
62  else
63  {
64 #ifdef REPORT_UNIMPLEMENTED_TYPE_CHECKS
65  std::cerr << "Unimplemented well-formedness check for type with id: "
66  << type.id_string() << std::endl;
67 #endif
68 
70  }
71 }
72 
81 void check_type(const typet &type, const validation_modet vm)
82 {
83  call_on_type<call_checkt>(type, vm);
84 }
85 
95  const typet &type,
96  const namespacet &ns,
97  const validation_modet vm)
98 {
99  call_on_type<call_validatet>(type, ns, vm);
100 }
101 
111  const typet &type,
112  const namespacet &ns,
113  const validation_modet vm)
114 {
115  call_on_type<call_validate_fullt>(type, ns, vm);
116 }
CALL_ON_TYPE
#define CALL_ON_TYPE(type_type)
Definition: validate_types.cpp:21
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:110
reference_typet
The reference type.
Definition: std_types.h:1560
typet
The type of an expression, extends irept.
Definition: type.h:28
floatbv_typet
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1386
namespace.h
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1223
type.h
Defines typet, type_with_subtypet and type_with_subtypest.
c_bool_typet
The C/C++ Booleans.
Definition: std_types.h:1618
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
call_on_type
void call_on_type(const typet &type, Args &&... args)
Definition: validate_types.cpp:25
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:81
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: std_types.h:1272
std_types.h
Pre-defined types.
irept::id_string
const std::string & id_string() const
Definition: irep.h:410
validation_modet
validation_modet
Definition: validation_mode.h:13
irept::id
const irep_idt & id() const
Definition: irep.h:407
fixedbv_typet
Fixed-width bit-vector with signed fixed-point interpretation.
Definition: std_types.h:1325
array_typet
Arrays with given size.
Definition: std_types.h:968
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:94
validate_helpers.h
validate.h
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1495
validate_types.h
bv_typet
Fixed-width bit-vector without numerical interpretation.
Definition: std_types.h:1113