Skip to content

Commit

Permalink
[fix] Incremental DT with no frames
Browse files Browse the repository at this point in the history
  • Loading branch information
Columpio committed Sep 26, 2023
1 parent 026da46 commit fb6dde0
Show file tree
Hide file tree
Showing 2 changed files with 2,783 additions and 6 deletions.
14 changes: 8 additions & 6 deletions include/klee/ADT/Incremental.h
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,11 @@ void extend(std::vector<_Tp, _Alloc> &ths,
ths.insert(ths.end(), other.begin(), other.end());
}

template <typename _Tp, typename _Alloc>
void takeAfterv(std::vector<_Tp, _Alloc> &ths, size_t n) {
std::vector<_Tp, _Alloc>(ths.begin() + n, ths.end()).swap(ths);
}

template <typename _Tp, typename _Alloc = std::allocator<_Tp>>
class inc_vector {
public:
Expand Down Expand Up @@ -131,12 +136,9 @@ class inc_vector {
size_t frames_count, frame_index;
take(n, frames_count, frame_index);
result = *this;
std::vector<_Tp, _Alloc>(result.v.begin() + n, result.v.end())
.swap(result.v);
std::vector<size_t>(result.frame_sizes.begin() + frame_index,
result.frame_sizes.end())
.swap(result.frame_sizes);
if (frames_count)
takeAfterv(result.v, n);
takeAfterv(result.frame_sizes, frame_index);
if (frames_count && !result.frame_sizes.empty())
result.frame_sizes[0] -= frames_count;
}

Expand Down
Loading

0 comments on commit fb6dde0

Please sign in to comment.