cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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
{
28
CALL_ON_CODE
(
code_assignt
);
29
}
30
else
if
(code.
get_statement
() == ID_decl)
31
{
32
CALL_ON_CODE
(
code_declt
);
33
}
34
else
if
(code.
get_statement
() == ID_dead)
35
{
36
CALL_ON_CODE
(
code_deadt
);
37
}
38
else
if
(code.
get_statement
() == ID_function_call)
39
{
40
CALL_ON_CODE
(
code_function_callt
);
41
}
42
else
if
(code.
get_statement
() == ID_return)
43
{
44
CALL_ON_CODE
(
code_returnt
);
45
}
46
else
if
(code.
get_statement
() == ID_block)
47
{
48
CALL_ON_CODE
(
code_blockt
);
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
58
CALL_ON_CODE
(
codet
);
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
84
void
validate_code
(
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
100
void
validate_full_code
(
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
}
code_assignt
A goto_instruction_codet representing an assignment in the program.
Definition
goto_instruction_code.h:22
code_blockt
A codet representing sequential composition of program statements.
Definition
std_code.h:130
code_deadt
A goto_instruction_codet representing the removal of a local variable going out of scope.
Definition
goto_instruction_code.h:131
code_declt
A goto_instruction_codet representing the declaration of a local variable.
Definition
goto_instruction_code.h:204
code_function_callt
goto_instruction_codet representation of a function call statement.
Definition
goto_instruction_code.h:271
code_returnt
goto_instruction_codet representation of a "return from afunction" statement.
Definition
goto_instruction_code.h:494
codet
Data structure for representing an arbitrary statement in a program.
Definition
std_code_base.h:29
codet::get_statement
const irep_idt & get_statement() const
Definition
std_code_base.h:65
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition
namespace.h:91
goto_instruction_code.h
std_code.h
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:84
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:100
CALL_ON_CODE
#define CALL_ON_CODE(code_type)
Definition
validate_code.cpp:20
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:70
call_on_code
void call_on_code(const codet &code, Args &&... args)
Definition
validate_code.cpp:24
validate_code.h
validate_helpers.h
validation_modet
validation_modet
Definition
validation_mode.h:13
goto-programs
validate_code.cpp
Generated by
1.17.0