Skip to content

Commit dc696a4

Browse files
Make format_number_range function instead of class
1 parent 678218a commit dc696a4

File tree

3 files changed

+4
-9
lines changed

3 files changed

+4
-9
lines changed

src/goto-instrument/cover_basic_blocks.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -223,7 +223,6 @@ void cover_basic_blockst::update_covered_lines(block_infot &block_info)
223223
INVARIANT(!cover_set.empty(), "covered lines set must not be empty");
224224
std::vector<unsigned> line_list(cover_set.begin(), cover_set.end());
225225

226-
format_number_ranget format_lines;
227-
std::string covered_lines = format_lines(line_list);
226+
std::string covered_lines = format_number_range(line_list);
228227
block_info.source_location.set_basic_block_covered_lines(covered_lines);
229228
}

src/util/format_number_range.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -16,9 +16,9 @@ Author: Daniel Kroening, [email protected]
1616
#include "format_number_range.h"
1717

1818
/// create shorter representation for output
19-
/// \par parameters: vector of numbers
19+
/// \param parameters: vector of numbers
2020
/// \return string of compressed number range representation
21-
std::string format_number_ranget::operator()(std::vector<unsigned> &numbers)
21+
std::string format_number_range(std::vector<unsigned> &numbers)
2222
{
2323
std::string number_range;
2424
std::sort(numbers.begin(), numbers.end());

src/util/format_number_range.h

+1-5
Original file line numberDiff line numberDiff line change
@@ -15,10 +15,6 @@ Author: Daniel Kroening, [email protected]
1515
#include <string>
1616
#include <vector>
1717

18-
class format_number_ranget
19-
{
20-
public:
21-
std::string operator()(std::vector<unsigned> &);
22-
};
18+
std::string format_number_range(std::vector<unsigned> &);
2319

2420
#endif // CPROVER_UTIL_FORMAT_NUMBER_RANGE_H

0 commit comments

Comments
 (0)