CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
validate_types.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Validate types
4
5Author: 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
22template <template <typename, typename> class C, typename... Args>
23void 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
79void check_type(const typet &type, const validation_modet vm)
80{
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{
114}
Pre-defined bitvector types.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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:391
const irep_idt & id() const
Definition irep.h:388
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
The reference type.
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