cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
inlining_decorator.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Utility functions for code contracts.
4
5
Author: Remi Delmas, delmasrd@amazon.com
6
7
Date: August 2022
8
9
\*******************************************************************/
10
11
#include "
inlining_decorator.h
"
12
13
inlining_decoratort::inlining_decoratort
(
message_handlert
&_wrapped)
14
:
wrapped
(_wrapped),
15
no_body_regex
(
std
::regex(
".*no body for function '(.*)'.*"
)),
16
missing_function_regex
(
17
std
::regex(
".*missing function '(.*)' is ignored.*"
)),
18
recursive_call_regex
(
19
std
::regex(
".*recursion is ignored on call to '(.*)'.*"
)),
20
not_enough_arguments_regex
(
21
std
::regex(
".*call to '(.*)': not enough arguments.*"
))
22
{
23
}
24
25
void
inlining_decoratort::match_no_body_warning
(
const
std::string &message)
26
{
27
std::smatch sm;
28
std::regex_match(message, sm,
no_body_regex
);
29
if
(sm.size() == 2)
30
no_body_set
.insert(sm.str(1));
31
}
32
33
void
inlining_decoratort::match_missing_function_warning
(
34
const
std::string &message)
35
{
36
std::smatch sm;
37
std::regex_match(message, sm,
missing_function_regex
);
38
if
(sm.size() == 2)
39
missing_function_set
.insert(sm.str(1));
40
}
41
42
void
inlining_decoratort::match_recursive_call_warning
(
43
const
std::string &message)
44
{
45
std::smatch sm;
46
std::regex_match(message, sm,
recursive_call_regex
);
47
if
(sm.size() == 2)
48
recursive_call_set
.insert(sm.str(1));
49
}
50
51
void
inlining_decoratort::match_not_enough_arguments_warning
(
52
const
std::string &message)
53
{
54
std::smatch sm;
55
std::regex_match(message, sm,
not_enough_arguments_regex
);
56
if
(sm.size() == 2)
57
not_enough_arguments_set
.insert(sm.str(1));
58
}
59
60
void
inlining_decoratort::parse_message
(
const
std::string &message)
61
{
62
match_no_body_warning
(message);
63
match_missing_function_warning
(message);
64
match_recursive_call_warning
(message);
65
match_not_enough_arguments_warning
(message);
66
}
67
68
void
inlining_decoratort::throw_on_no_body
(
messaget
&log,
const
int
error_code)
69
{
70
if
(
no_body_set
.size() != 0)
71
{
72
for
(
auto
it :
no_body_set
)
73
{
74
log.
error
() <<
"No body for '"
<< it <<
"' during inlining"
75
<<
messaget::eom
;
76
}
77
throw
error_code;
78
}
79
}
80
81
void
inlining_decoratort::throw_on_recursive_calls
(
82
messaget
&log,
83
const
int
error_code)
84
{
85
if
(
recursive_call_set
.size() != 0)
86
{
87
for
(
auto
it :
recursive_call_set
)
88
{
89
log.
error
() <<
"Recursive call to '"
<< it <<
"' during inlining"
90
<<
messaget::eom
;
91
}
92
throw
error_code;
93
}
94
}
95
96
void
inlining_decoratort::throw_on_missing_function
(
97
messaget
&log,
98
const
int
error_code)
99
{
100
if
(
missing_function_set
.size() != 0)
101
{
102
for
(
auto
it :
missing_function_set
)
103
{
104
log.
error
() <<
"Missing function '"
<< it <<
"' during inlining"
105
<<
messaget::eom
;
106
}
107
throw
error_code;
108
}
109
}
110
111
void
inlining_decoratort::throw_on_not_enough_arguments
(
112
messaget
&log,
113
const
int
error_code)
114
{
115
if
(
not_enough_arguments_set
.size() != 0)
116
{
117
for
(
auto
it :
not_enough_arguments_set
)
118
{
119
log.
error
() <<
"Not enough arguments for '"
<< it <<
"' during inlining"
120
<<
messaget::eom
;
121
}
122
throw
error_code;
123
}
124
}
inlining_decoratort::not_enough_arguments_set
std::set< irep_idt > not_enough_arguments_set
Definition
inlining_decorator.h:62
inlining_decoratort::throw_on_recursive_calls
void throw_on_recursive_calls(messaget &log, const int error_code)
Throws the given error code if recursive call warnings happend during inlining.
Definition
inlining_decorator.cpp:81
inlining_decoratort::inlining_decoratort
inlining_decoratort(message_handlert &_wrapped)
Definition
inlining_decorator.cpp:13
inlining_decoratort::throw_on_missing_function
void throw_on_missing_function(messaget &log, const int error_code)
Throws the given error code if missing function warnings happend during inlining.
Definition
inlining_decorator.cpp:96
inlining_decoratort::no_body_set
std::set< irep_idt > no_body_set
Definition
inlining_decorator.h:47
inlining_decoratort::missing_function_regex
std::regex missing_function_regex
Definition
inlining_decorator.h:51
inlining_decoratort::recursive_call_regex
std::regex recursive_call_regex
Definition
inlining_decorator.h:56
inlining_decoratort::missing_function_set
std::set< irep_idt > missing_function_set
Definition
inlining_decorator.h:52
inlining_decoratort::wrapped
message_handlert & wrapped
Definition
inlining_decorator.h:44
inlining_decoratort::match_no_body_warning
void match_no_body_warning(const std::string &message)
Definition
inlining_decorator.cpp:25
inlining_decoratort::throw_on_no_body
void throw_on_no_body(messaget &log, const int error_code)
Throws the given error code if no body for function warnings happend during inlining.
Definition
inlining_decorator.cpp:68
inlining_decoratort::match_recursive_call_warning
void match_recursive_call_warning(const std::string &message)
Definition
inlining_decorator.cpp:42
inlining_decoratort::match_not_enough_arguments_warning
void match_not_enough_arguments_warning(const std::string &message)
Definition
inlining_decorator.cpp:51
inlining_decoratort::recursive_call_set
std::set< irep_idt > recursive_call_set
Definition
inlining_decorator.h:57
inlining_decoratort::throw_on_not_enough_arguments
void throw_on_not_enough_arguments(messaget &log, const int error_code)
Throws the given error code if not enough arguments warnings happend during inlining.
Definition
inlining_decorator.cpp:111
inlining_decoratort::not_enough_arguments_regex
std::regex not_enough_arguments_regex
Definition
inlining_decorator.h:61
inlining_decoratort::match_missing_function_warning
void match_missing_function_warning(const std::string &message)
Definition
inlining_decorator.cpp:33
inlining_decoratort::parse_message
void parse_message(const std::string &message)
Definition
inlining_decorator.cpp:60
inlining_decoratort::no_body_regex
std::regex no_body_regex
Definition
inlining_decorator.h:46
message_handlert::message_handlert
message_handlert()
Definition
message.h:29
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition
message.h:154
messaget::error
mstreamt & error() const
Definition
message.h:391
messaget::eom
static eomt eom
Definition
message.h:289
inlining_decorator.h
std
STL namespace.
goto-instrument
contracts
inlining_decorator.cpp
Generated by
1.17.0