CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
validate_code.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Validate code
4
5Author: 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
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
23template <template <typename, typename> class C, typename... Args>
24void 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
70void check_code(const codet &code, const validation_modet vm)
71{
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{
106}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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.
const irep_idt & get_statement() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
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