diff options
| author | Lukáš Zaoral <lzaoral@redhat.com> | 2022-04-17 13:32:15 +0200 |
|---|---|---|
| committer | MartinNowack <2443641+MartinNowack@users.noreply.github.com> | 2023-03-20 16:05:38 +0000 |
| commit | 1398e960ec9aca3f0ceac5e37062631986b9c2a8 (patch) | |
| tree | ff7ed01317fa2ef90b9678c8ea1bc86fb94ba531 /include | |
| parent | d9da9eadbc0aacf61b336231560abb67bcba91ad (diff) | |
| download | klee-1398e960ec9aca3f0ceac5e37062631986b9c2a8.tar.gz | |
ConstantArrayExprVisitor: Fix detection of multiple array indices
Previously, the code did two consecutive checks. First one succeeded only if the given index was not already seen and the second one did an analogous check but for arrays. However, if the given index usage was already detected for some array, its usage for another array that already had some other index detected would be silently skipped and the `incompatible` flag would not be set. Therefore, if the code contained e.g. the following conditional jump on two arrays with two symbolic indices, the multi-index access would remain undetected: if ((array1[k] + array2[x] + array2[k]) == 0) Resulting in the following output: KLEE: WARNING: OPT_I: infeasible branch! KLEE: WARNING: OPT_I: successful
Diffstat (limited to 'include')
| -rw-r--r-- | include/klee/Expr/ArrayExprVisitor.h | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/include/klee/Expr/ArrayExprVisitor.h b/include/klee/Expr/ArrayExprVisitor.h index 28f485d9..b2941e42 100644 --- a/include/klee/Expr/ArrayExprVisitor.h +++ b/include/klee/Expr/ArrayExprVisitor.h @@ -35,8 +35,6 @@ class ConstantArrayExprVisitor : public ExprVisitor { private: using bindings_ty = std::map<const Array *, std::vector<ref<Expr>>>; bindings_ty &arrays; - // Avoids adding the same index twice - std::unordered_set<unsigned> addedIndexes; bool incompatible; protected: |