CBMC
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  {
28  }
29  else if(type.id() == ID_unsignedbv)
30  {
32  }
33  else if(type.id() == ID_signedbv)
34  {
36  }
37  else if(type.id() == ID_fixedbv)
38  {
40  }
41  else if(type.id() == ID_floatbv)
42  {
44  }
45  else if(type.id() == ID_pointer)
46  {
47  if(type.get_bool(ID_C_reference))
49  else
51  }
52  else if(type.id() == ID_c_bool)
53  {
55  }
56  else if(type.id() == ID_array)
57  {
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 
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 
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 
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 }
Pre-defined bitvector types.
Arrays with given size.
Definition: std_types.h:807
Fixed-width bit-vector without numerical interpretation.
The C/C++ Booleans.
Definition: c_types.h:97
Fixed-width bit-vector with signed fixed-point interpretation.
Fixed-width bit-vector with IEEE floating-point interpretation.
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:57
const std::string & id_string() const
Definition: irep.h:387
const irep_idt & id() const
Definition: irep.h:384
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
The reference type.
Definition: pointer_expr.h:121
Fixed-width bit-vector with two's complement interpretation.
The type of an expression, extends irept.
Definition: type.h:29
Fixed-width bit-vector with unsigned binary interpretation.
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)
#define CALL_ON_TYPE(type_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...
void call_on_type(const typet &type, Args &&... args)
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)
validation_modet