diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 1fd2961591e..b1258d77d31 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -203,7 +203,10 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) options.set_option("depth", cmdline.get_value("depth")); if(cmdline.isset("unwindset")) - options.set_option("unwindset", cmdline.get_value("unwindset")); + { + options.set_option( + "unwindset", cmdline.get_comma_separated_values("unwindset")); + } // constant propagation if(cmdline.isset("no-propagation")) diff --git a/regression/goto-instrument/unwind-unwindset4/test.desc b/regression/goto-instrument/unwind-unwindset4/test.desc index 5eaca992f1b..d9c3f7874a9 100644 --- a/regression/goto-instrument/unwind-unwindset4/test.desc +++ b/regression/goto-instrument/unwind-unwindset4/test.desc @@ -1,6 +1,6 @@ CORE main.c ---unwindset main.0:10,f.0:10,g.0:10,g.1:10 --unwinding-assertions +--unwindset main.0:10,f.0:10 --unwindset g.0:10,g.1:10 --unwinding-assertions ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/memory-analyzer/pointer_05/test.desc b/regression/memory-analyzer/pointer_05/test.desc index fffea4459e4..400f2b8fe1c 100644 --- a/regression/memory-analyzer/pointer_05/test.desc +++ b/regression/memory-analyzer/pointer_05/test.desc @@ -1,5 +1,5 @@ CORE main.gb ---breakpoint checkpoint --symbols p1,x,p2 +--breakpoint checkpoint --symbols p1,x --symbols p2 ^EXIT=0$ ^SIGNAL=0$ diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index cf8d0cdc63a..a05f909e2de 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -255,7 +255,10 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) } if(cmdline.isset("unwindset")) - options.set_option("unwindset", cmdline.get_values("unwindset")); + { + options.set_option( + "unwindset", cmdline.get_comma_separated_values("unwindset")); + } // constant propagation if(cmdline.isset("no-propagation")) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 1c879bc3610..6d635ccedeb 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -186,7 +186,8 @@ int goto_instrument_parse_optionst::doit() if(unwindset_given) { unwindset.parse_unwindset( - cmdline.get_values("unwindset"), ui_message_handler); + cmdline.get_comma_separated_values("unwindset"), + ui_message_handler); } bool unwinding_assertions=cmdline.isset("unwinding-assertions"); diff --git a/src/goto-instrument/unwindset.cpp b/src/goto-instrument/unwindset.cpp index 7b0168ccdd0..5b79a560bff 100644 --- a/src/goto-instrument/unwindset.cpp +++ b/src/goto-instrument/unwindset.cpp @@ -179,13 +179,7 @@ void unwindsett::parse_unwindset( message_handlert &message_handler) { for(auto &element : unwindset) - { - std::vector unwindset_elements = - split_string(element, ',', true, true); - - for(auto &element : unwindset_elements) - parse_unwindset_one_loop(element, message_handler); - } + parse_unwindset_one_loop(element, message_handler); } optionalt diff --git a/src/memory-analyzer/analyze_symbol.cpp b/src/memory-analyzer/analyze_symbol.cpp index 565285ebfe2..b1361497555 100644 --- a/src/memory-analyzer/analyze_symbol.cpp +++ b/src/memory-analyzer/analyze_symbol.cpp @@ -106,7 +106,8 @@ mp_integer gdb_value_extractort::get_type_size(const typet &type) const return *maybe_size / CHAR_BIT; } -void gdb_value_extractort::analyze_symbols(const std::vector &symbols) +void gdb_value_extractort::analyze_symbols( + const std::list &symbols) { // record addresses of given symbols for(const auto &id : symbols) diff --git a/src/memory-analyzer/analyze_symbol.h b/src/memory-analyzer/analyze_symbol.h index 03bd588f92a..6ded9b196ae 100644 --- a/src/memory-analyzer/analyze_symbol.h +++ b/src/memory-analyzer/analyze_symbol.h @@ -44,7 +44,7 @@ class gdb_value_extractort /// \ref symbol_exprt (via the `values` map) and then call /// \ref analyze_symbol on it. /// \param symbols: names of symbols to be analysed - void analyze_symbols(const std::vector &symbols); + void analyze_symbols(const std::list &symbols); /// Get memory snapshot as C code /// \return converted block of code with the collected assignments diff --git a/src/memory-analyzer/memory_analyzer_parse_options.cpp b/src/memory-analyzer/memory_analyzer_parse_options.cpp index 124e941e942..dcb0dc6de3f 100644 --- a/src/memory-analyzer/memory_analyzer_parse_options.cpp +++ b/src/memory-analyzer/memory_analyzer_parse_options.cpp @@ -15,7 +15,6 @@ Author: Malte Mues #include #include #include -#include #include #include @@ -103,9 +102,6 @@ int memory_analyzer_parse_optionst::doit() std::string binary = cmdline.args.front(); - const std::string symbol_list(cmdline.get_value("symbols")); - std::vector result = split_string(symbol_list, ',', true, true); - auto opt = read_goto_binary(binary, ui_message_handler); if(!opt.has_value()) @@ -131,12 +127,8 @@ int memory_analyzer_parse_optionst::doit() gdb_value_extractor.run_gdb_to_breakpoint(breakpoint); } - std::vector result_ids(result.size()); - std::transform( - result.begin(), result.end(), result_ids.begin(), [](std::string &name) { - return irep_idt{name}; - }); - gdb_value_extractor.analyze_symbols(result_ids); + gdb_value_extractor.analyze_symbols( + cmdline.get_comma_separated_values("symbols")); std::ofstream file;