CBMC
validate_helpers.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto program validation helper templates
4 
5 Author: Daniel Poetzl
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_UTIL_VALIDATE_HELPERS_H
10 #define CPROVER_UTIL_VALIDATE_HELPERS_H
11 
12 #include <type_traits>
13 
14 class namespacet;
15 enum class validation_modet;
16 
17 template <typename Base, typename T>
18 struct call_checkt
19 {
20  static_assert(
21  std::is_base_of<Base, T>::value,
22  "T should be derived from Base");
23 
24  void operator()(const Base &base, const validation_modet vm)
25  {
26  T::check(base, vm);
27  }
28 };
29 
30 template <typename Base, typename T>
31 struct call_validatet
32 {
33  static_assert(
34  std::is_base_of<Base, T>::value,
35  "T should be derived from Base");
36 
37  void
38  operator()(const Base &base, const namespacet &ns, const validation_modet vm)
39  {
40  T::validate(base, ns, vm);
41  }
42 };
43 
44 template <typename Base, typename T>
45 struct call_validate_fullt
46 {
47  static_assert(
48  std::is_base_of<Base, T>::value,
49  "T should be derived from Base");
50 
51  void
52  operator()(const Base &base, const namespacet &ns, const validation_modet vm)
53  {
54  T::validate_full(base, ns, vm);
55  }
56 };
57 
58 #endif /* CPROVER_UTIL_VALIDATE_HELPERS_H */
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
validate
static bool validate(const string_refinementt::infot &info)
Definition: string_refinement.cpp:150
call_checkt
Definition: validate_helpers.h:19
call_checkt::operator()
void operator()(const Base &base, const validation_modet vm)
Definition: validate_helpers.h:24
call_validate_fullt
Definition: validate_helpers.h:46
call_validate_fullt::operator()
void operator()(const Base &base, const namespacet &ns, const validation_modet vm)
Definition: validate_helpers.h:52
call_validatet
Definition: validate_helpers.h:32
call_validatet::operator()
void operator()(const Base &base, const namespacet &ns, const validation_modet vm)
Definition: validate_helpers.h:38
validation_modet
validation_modet
Definition: validation_mode.h:13