@@ -29,6 +29,7 @@ Author: Daniel Kroening, dkr@amazon.com
2929#include < fstream>
3030#include < iostream>
3131#include < map>
32+ #include < regex>
3233#include < sstream>
3334#include < unordered_map>
3435
@@ -86,7 +87,7 @@ struct c_wranglert
8687 bool remove_static = false ;
8788 };
8889
89- using functionst = std::map <std::string , functiont>;
90+ using functionst = std::list <std::pair<std::regex , functiont> >;
9091 functionst functions;
9192
9293 // output
@@ -171,6 +172,9 @@ void c_wranglert::configure_functions(const jsont &config)
171172 if (!items.is_array ())
172173 throw deserialization_exceptiont (" function entry must be sequence" );
173174
175+ this ->functions .emplace_back (function_name, functiont{});
176+ functiont &function_config = this ->functions .back ().second ;
177+
174178 for (const auto &function_item : to_json_array (items))
175179 {
176180 // These need to start with "ensures", "requires", "assigns",
@@ -190,16 +194,14 @@ void c_wranglert::configure_functions(const jsont &config)
190194 std::ostringstream rest;
191195 join_strings (rest, split.begin () + 1 , split.end (), ' ' );
192196
193- this ->functions [function_name].contract .emplace_back (
194- split[0 ], rest.str ());
197+ function_config.contract .emplace_back (split[0 ], rest.str ());
195198 }
196199 else if (split[0 ] == " assert" && split.size () >= 3 )
197200 {
198201 std::ostringstream rest;
199202 join_strings (rest, split.begin () + 2 , split.end (), ' ' );
200203
201- this ->functions [function_name].assertions .emplace_back (
202- split[1 ], rest.str ());
204+ function_config.assertions .emplace_back (split[1 ], rest.str ());
203205 }
204206 else if (
205207 (split[0 ] == " for" && split.size () >= 3 && split[2 ] == " invariant" ) ||
@@ -208,23 +210,23 @@ void c_wranglert::configure_functions(const jsont &config)
208210 std::ostringstream rest;
209211 join_strings (rest, split.begin () + 3 , split.end (), ' ' );
210212
211- this -> functions [function_name] .loop_invariants .emplace_back (
213+ function_config .loop_invariants .emplace_back (
212214 split[0 ], split[1 ], rest.str ());
213215 }
214216 else if (split[0 ] == " stub" )
215217 {
216218 std::ostringstream rest;
217219 join_strings (rest, split.begin () + 1 , split.end (), ' ' );
218220
219- this -> functions [function_name] .stub = rest.str ();
221+ function_config .stub = rest.str ();
220222 }
221223 else if (split[0 ] == " remove" )
222224 {
223225 if (split.size () == 1 )
224226 throw deserialization_exceptiont (" unexpected remove entry" );
225227
226228 if (split[1 ] == " static" )
227- this -> functions [function_name] .remove_static = true ;
229+ function_config .remove_static = true ;
228230 else
229231 throw deserialization_exceptiont (
230232 " unexpected remove entry " + split[1 ]);
@@ -401,13 +403,15 @@ static void mangle(
401403 if (
402404 declaration.is_function () && name_opt.has_value () && declaration.has_body ())
403405 {
404- auto f_it = config.functions .find (name_opt->text );
405- if (f_it != config.functions .end ())
406+ for (const auto &entry : config.functions )
406407 {
407- // we are to modify this function
408- mangle_function (declaration, defines, f_it->second , out);
408+ if (std::regex_match (name_opt->text , entry.first ))
409+ {
410+ // we are to modify this function
411+ mangle_function (declaration, defines, entry.second , out);
409412
410- return ;
413+ return ;
414+ }
411415 }
412416 }
413417
0 commit comments