CBMC
Loading...
Searching...
No Matches
inlining_decorator.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Utility functions for code contracts.
4
5Author: Remi Delmas, delmasrd@amazon.com
6
7Date: August 2022
8
9\*******************************************************************/
10
11#include "inlining_decorator.h"
12
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
25void 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
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
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
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
67
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"
76 }
77 throw error_code;
78 }
79}
80
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"
91 }
92 throw error_code;
93 }
94}
95
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
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}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
std::set< irep_idt > not_enough_arguments_set
void throw_on_recursive_calls(messaget &log, const int error_code)
Throws the given error code if recursive call warnings happend during inlining.
inlining_decoratort(message_handlert &_wrapped)
void throw_on_missing_function(messaget &log, const int error_code)
Throws the given error code if missing function warnings happend during inlining.
std::set< irep_idt > no_body_set
std::regex missing_function_regex
std::set< irep_idt > missing_function_set
void match_no_body_warning(const std::string &message)
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.
void match_recursive_call_warning(const std::string &message)
void match_not_enough_arguments_warning(const std::string &message)
std::set< irep_idt > recursive_call_set
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.
std::regex not_enough_arguments_regex
void match_missing_function_warning(const std::string &message)
void parse_message(const std::string &message)
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
static eomt eom
Definition message.h:289
double log(double x)
Definition math.c:2449
STL namespace.