cprover
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 "std_code.h"
16 #include "validate_helpers.h"
17 
18 #define CALL_ON_CODE(code_type) \
19  C<codet, code_type>()(code, std::forward<Args>(args)...)
20 
21 template <template <typename, typename> class C, typename... Args>
22 void call_on_code(const codet &code, Args &&... args)
23 {
24  if(code.get_statement() == ID_assign)
25  {
27  }
28  else if(code.get_statement() == ID_decl)
29  {
31  }
32  else if(code.get_statement() == ID_dead)
33  {
35  }
36  else if(code.get_statement() == ID_function_call)
37  {
39  }
40  else if(code.get_statement() == ID_return)
41  {
43  }
44  else if(code.get_statement() == ID_block)
45  {
47  }
48  else
49  {
50 #ifdef REPORT_UNIMPLEMENTED_CODE_CHECKS
51  std::cerr << "Unimplemented well-formedness check for code statement with "
52  "id: "
53  << code.get_statement().id_string() << std::endl;
54 #endif
55 
57  }
58 }
59 
68 void check_code(const codet &code, const validation_modet vm)
69 {
70  call_on_code<call_checkt>(code, vm);
71 }
72 
83  const codet &code,
84  const namespacet &ns,
85  const validation_modet vm)
86 {
87  call_on_code<call_validatet>(code, ns, vm);
88 }
89 
99  const codet &code,
100  const namespacet &ns,
101  const validation_modet vm)
102 {
103  call_on_code<call_validate_fullt>(code, ns, vm);
104 }
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:168
validate_code
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,...
Definition: validate_code.cpp:82
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:400
call_on_code
void call_on_code(const codet &code, Args &&... args)
Definition: validate_code.cpp:22
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1213
validate_full_code
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...
Definition: validate_code.cpp:98
validation_modet
validation_modet
Definition: validation_mode.h:13
code_deadt
A codet representing the removal of a local variable going out of scope.
Definition: std_code.h:497
std_code.h
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1340
check_code
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,...
Definition: validate_code.cpp:68
validate_helpers.h
CALL_ON_CODE
#define CALL_ON_CODE(code_type)
Definition: validate_code.cpp:18
validate_code.h
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:293
codet::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:69
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33