CBMC
validate_code.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Validate code
4 
5 Author: Daniel Poetzl
6 
7 \*******************************************************************/
8 
9 #include "validate_code.h"
10 
11 #ifdef REPORT_UNIMPLEMENTED_CODE_CHECKS
12 # include <iostream>
13 #endif
14 
15 #include <util/std_code.h> // IWYU pragma: keep
16 #include <util/validate_helpers.h>
17 
18 #include "goto_instruction_code.h" // IWYU pragma: keep
19 
20 #define CALL_ON_CODE(code_type) \
21  C<codet, code_type>()(code, std::forward<Args>(args)...)
22 
23 template <template <typename, typename> class C, typename... Args>
24 void call_on_code(const codet &code, Args &&... args)
25 {
26  if(code.get_statement() == ID_assign)
27  {
29  }
30  else if(code.get_statement() == ID_decl)
31  {
33  }
34  else if(code.get_statement() == ID_dead)
35  {
37  }
38  else if(code.get_statement() == ID_function_call)
39  {
41  }
42  else if(code.get_statement() == ID_return)
43  {
45  }
46  else if(code.get_statement() == ID_block)
47  {
49  }
50  else
51  {
52 #ifdef REPORT_UNIMPLEMENTED_CODE_CHECKS
53  std::cerr << "Unimplemented well-formedness check for code statement with "
54  "id: "
55  << code.get_statement().id_string() << std::endl;
56 #endif
57 
59  }
60 }
61 
70 void check_code(const codet &code, const validation_modet vm)
71 {
72  call_on_code<call_checkt>(code, vm);
73 }
74 
85  const codet &code,
86  const namespacet &ns,
87  const validation_modet vm)
88 {
89  call_on_code<call_validatet>(code, ns, vm);
90 }
91 
101  const codet &code,
102  const namespacet &ns,
103  const validation_modet vm)
104 {
105  call_on_code<call_validate_fullt>(code, ns, vm);
106 }
A goto_instruction_codet representing an assignment in the program.
A codet representing sequential composition of program statements.
Definition: std_code.h:130
A goto_instruction_codet representing the removal of a local variable going out of scope.
A goto_instruction_codet representing the declaration of a local variable.
goto_instruction_codet representation of a function call statement.
goto_instruction_codet representation of a "return from a function" statement.
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
const irep_idt & get_statement() const
Definition: std_code_base.h:65
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
void validate_code(const codet &code, const namespacet &ns, const validation_modet vm)
Check that the given code statement is well-formed, assuming that all its enclosed statements,...
void validate_full_code(const codet &code, const namespacet &ns, const validation_modet vm)
Check that the given code statement is well-formed (full check, including checks of all subexpression...
#define CALL_ON_CODE(code_type)
void check_code(const codet &code, const validation_modet vm)
Check that the given code statement is well-formed (shallow checks only, i.e., enclosed statements,...
void call_on_code(const codet &code, Args &&... args)
validation_modet