CBMC
inlining_decorator.h
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 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_INLINING_DECORATOR_H
12 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_INLINING_DECORATOR_H
13 
14 #include <util/irep.h>
15 #include <util/message.h>
16 
17 #include <regex>
18 #include <set>
19 
42 {
43 private:
45 
46  std::regex no_body_regex;
47  std::set<irep_idt> no_body_set;
48 
49  void match_no_body_warning(const std::string &message);
50 
52  std::set<irep_idt> missing_function_set;
53 
54  void match_missing_function_warning(const std::string &message);
55 
57  std::set<irep_idt> recursive_call_set;
58 
59  void match_recursive_call_warning(const std::string &message);
60 
62  std::set<irep_idt> not_enough_arguments_set;
63 
64  void match_not_enough_arguments_warning(const std::string &message);
65 
66  void parse_message(const std::string &message);
67 
68 public:
69  explicit inlining_decoratort(message_handlert &_wrapped);
70 
73  void throw_on_no_body(messaget &log, const int error_code);
74 
77  void throw_on_recursive_calls(messaget &log, const int error_code);
78 
81  void throw_on_missing_function(messaget &log, const int error_code);
82 
85  void throw_on_not_enough_arguments(messaget &log, const int error_code);
86 
87  const std::set<irep_idt> &get_no_body_set() const
88  {
89  return no_body_set;
90  }
91 
92  const std::set<irep_idt> &get_missing_function_set() const
93  {
94  return missing_function_set;
95  }
96 
97  const std::set<irep_idt> &get_recursive_call_set() const
98  {
99  return recursive_call_set;
100  }
101 
102  const std::set<irep_idt> &get_not_enough_arguments_set() const
103  {
105  }
106 
107  void print(unsigned level, const std::string &message) override
108  {
109  parse_message(message);
110  wrapped.print(level, message);
111  }
112 
113  void print(unsigned level, const xmlt &xml) override
114  {
115  wrapped.print(level, xml);
116  }
117 
118  void print(unsigned level, const jsont &json) override
119  {
120  wrapped.print(level, json);
121  }
122 
123  void print(unsigned level, const structured_datat &data) override
124  {
125  wrapped.print(level, data);
126  }
127 
128  void print(
129  unsigned level,
130  const std::string &message,
131  const source_locationt &location) override
132  {
133  parse_message(message);
134  wrapped.print(level, message, location);
135  return;
136  }
137 
138  void flush(unsigned i) override
139  {
140  return wrapped.flush(i);
141  }
142 
143  void set_verbosity(unsigned _verbosity)
144  {
145  wrapped.set_verbosity(_verbosity);
146  }
147 
148  unsigned get_verbosity() const
149  {
150  return wrapped.get_verbosity();
151  }
152 
153  std::size_t get_message_count(unsigned level) const
154  {
155  return wrapped.get_message_count(level);
156  }
157 
158  std::string command(unsigned i) const override
159  {
160  return wrapped.command(i);
161  }
162 };
163 
164 #endif
Decorator for a message_handlert used during function inlining that collect names of GOTO functions c...
void print(unsigned level, const std::string &message) override
const std::set< irep_idt > & get_no_body_set() const
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.
const std::set< irep_idt > & get_missing_function_set() const
unsigned get_verbosity() const
void print(unsigned level, const jsont &json) override
void set_verbosity(unsigned _verbosity)
void print(unsigned level, const std::string &message, const source_locationt &location) override
void flush(unsigned i) override
void print(unsigned level, const xmlt &xml) override
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::regex recursive_call_regex
std::set< irep_idt > missing_function_set
message_handlert & wrapped
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 print(unsigned level, const structured_datat &data) override
std::string command(unsigned i) const override
Create an ECMA-48 SGR (Select Graphic Rendition) command.
void match_recursive_call_warning(const std::string &message)
void match_not_enough_arguments_warning(const std::string &message)
const std::set< irep_idt > & get_not_enough_arguments_set() const
std::size_t get_message_count(unsigned level) const
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
const std::set< irep_idt > & get_recursive_call_set() const
void match_missing_function_warning(const std::string &message)
void parse_message(const std::string &message)
Definition: json.h:27
void set_verbosity(unsigned _verbosity)
Definition: message.h:52
virtual void print(unsigned level, const std::string &message)=0
Definition: message.cpp:60
std::size_t get_message_count(unsigned level) const
Definition: message.h:55
unsigned get_verbosity() const
Definition: message.h:53
virtual std::string command(unsigned) const
Create an ECMA-48 SGR (Select Graphic Rendition) command.
Definition: message.h:65
virtual void flush(unsigned)=0
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:154
A way of representing nested key/value data.
Definition: xml.h:21
double log(double x)
Definition: math.c:2776
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:120
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:110