diff options
| author | vpushkar <vpushkar@ptsecurity.com> | 2016-03-16 15:54:26 +0300 |
|---|---|---|
| committer | vpushkar <vpushkar@ptsecurity.com> | 2016-03-16 15:54:26 +0300 |
| commit | bfc4714531978867a7f68a52f0b614b63f06a391 (patch) | |
| tree | 04aa7f6230271735c78645e60e47f6e91fe9b238 /lib/Core | |
| parent | 7366b149824a6c899fa804674574d5b21b5171a6 (diff) | |
| download | klee-bfc4714531978867a7f68a52f0b614b63f06a391.tar.gz | |
Wrong std::vector 'values' usage after vector's capacity reserve. It is the error to use [] operator for accessing vector's elements after reserving. In such cases push_back/emplace methods should be used. But in this source code the usage of std::vector is redundant. So vector 'values' was iliminated.
Diffstat (limited to 'lib/Core')
0 files changed, 0 insertions, 0 deletions