diff --git a/src/goto-instrument/unwindset.cpp b/src/goto-instrument/unwindset.cpp index 8c909af3213..5fd1627c556 100644 --- a/src/goto-instrument/unwindset.cpp +++ b/src/goto-instrument/unwindset.cpp @@ -54,19 +54,16 @@ void unwindsett::parse_unwindset_one_loop(std::string val) } } -void unwindsett::parse_unwindset(const std::string &unwindset) -{ - std::vector unwindset_elements = - split_string(unwindset, ',', true, true); - - for(auto &element : unwindset_elements) - parse_unwindset_one_loop(element); -} - void unwindsett::parse_unwindset(const std::list &unwindset) { for(auto &element : unwindset) - parse_unwindset(element); + { + std::vector unwindset_elements = + split_string(element, ',', true, true); + + for(auto &element : unwindset_elements) + parse_unwindset_one_loop(element); + } } optionalt @@ -104,5 +101,10 @@ void unwindsett::parse_unwindset_file(const std::string &file_name) std::stringstream buffer; buffer << file.rdbuf(); - parse_unwindset(buffer.str()); + + std::vector unwindset_elements = + split_string(buffer.str(), ',', true, true); + + for(auto &element : unwindset_elements) + parse_unwindset_one_loop(element); } diff --git a/src/goto-instrument/unwindset.h b/src/goto-instrument/unwindset.h index 8e35071f615..aa713adbe6e 100644 --- a/src/goto-instrument/unwindset.h +++ b/src/goto-instrument/unwindset.h @@ -16,7 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include @@ -32,10 +31,6 @@ class unwindsett // global limit for all loops void parse_unwind(const std::string &unwind); - // limit for instances of a loop - DEPRECATED(SINCE(2019, 11, 15, "use parse_unwindset(list) instead")) - void parse_unwindset(const std::string &unwindset); - // limit for instances of a loop void parse_unwindset(const std::list &unwindset);