Skip to content

Commit aa7528b

Browse files
Columpiomisonijnik
authored andcommitted
[fix] Incremental DT with no frames
1 parent 026da46 commit aa7528b

File tree

2 files changed

+2783
-6
lines changed

2 files changed

+2783
-6
lines changed

include/klee/ADT/Incremental.h

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,11 @@ void extend(std::vector<_Tp, _Alloc> &ths,
2828
ths.insert(ths.end(), other.begin(), other.end());
2929
}
3030

31+
template <typename _Tp, typename _Alloc>
32+
void takeAfterv(std::vector<_Tp, _Alloc> &ths, size_t n) {
33+
std::vector<_Tp, _Alloc>(ths.begin() + n, ths.end()).swap(ths);
34+
}
35+
3136
template <typename _Tp, typename _Alloc = std::allocator<_Tp>>
3237
class inc_vector {
3338
public:
@@ -131,12 +136,9 @@ class inc_vector {
131136
size_t frames_count, frame_index;
132137
take(n, frames_count, frame_index);
133138
result = *this;
134-
std::vector<_Tp, _Alloc>(result.v.begin() + n, result.v.end())
135-
.swap(result.v);
136-
std::vector<size_t>(result.frame_sizes.begin() + frame_index,
137-
result.frame_sizes.end())
138-
.swap(result.frame_sizes);
139-
if (frames_count)
139+
takeAfterv(result.v, n);
140+
takeAfterv(result.frame_sizes, frame_index);
141+
if (frames_count && !result.frame_sizes.empty())
140142
result.frame_sizes[0] -= frames_count;
141143
}
142144

0 commit comments

Comments
 (0)