[PATCH] D81254: [analyzer] Produce symbolic values for C-array elements

steakhal added a comment. In D81254#2218196 , @ASDenysPetrov wrote: >> We know where it points to (aka. the pointer's value is conjured), but we >> don't know what the value if there. > > Absolutely right. I looked at this patch after a while and don't

[PATCH] D81254: [analyzer] Produce symbolic values for C-array elements

ASDenysPetrov added a comment. Hey, folk, welcome to https://reviews.llvm.org/D85984 I've moved the logic of this checker in `PthreadLockChecker` Should this revision be //closed //or //rejected //somehow? CHANGES SINCE LAST ACTION https://reviews.llvm.org/D81254/new/

[PATCH] D81254: [analyzer] Produce symbolic values for C-array elements

ASDenysPetrov added a comment. @steakhal > If index1 and index2 has the same value, we should not be confident that the > x == y holds. Thanks! Now I see. Shame on me =) > We know where it points to (aka. the pointer's value is conjured), but we > don't know what the value if there.

[PATCH] D81254: [analyzer] Produce symbolic values for C-array elements

steakhal added a comment. In D81254#2122449 , @ASDenysPetrov wrote: > @NoQ, thanks for the examples. > > I didn't get the first one. How do you get to the "//In reality we don't > know//", if we don't touch `a[index1]`: If `index1` and `index2` has the

[PATCH] D81254: [analyzer] Produce symbolic values for C-array elements

ASDenysPetrov added a comment. @NoQ, thanks for the examples. I didn't get the first one. How do you get to the "//In reality we don't know//", if we don't touch `a[index1]`: void test1(int *a, int index1, int index2) { int x = a[index1]; a[index2] = 0; int y = a[index1];

[PATCH] D81254: [analyzer] Produce symbolic values for C-array elements

NoQ added a comment. Here are some examples: void test1(int *a, int index1, int index2) { int x = a[index1]; a[index2] = 0; int y = a[index1]; // In reality we don't know but after your patch // we're confident that this is "TRUE". clang_analyzer_eval(x == y); }

[PATCH] D81254: [analyzer] Produce symbolic values for C-array elements

ASDenysPetrov marked an inline comment as done. ASDenysPetrov added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RegionStore.cpp:1709 if (!O.getRegion()) -return UnknownVal(); +return svalBuilder.getRegionValueSymbolVal(R); NoQ wrote:

[PATCH] D81254: [analyzer] Produce symbolic values for C-array elements

ASDenysPetrov updated this revision to Diff 269481. ASDenysPetrov added a comment. Added more tests changing an array element. CHANGES SINCE LAST ACTION https://reviews.llvm.org/D81254/new/ https://reviews.llvm.org/D81254 Files: clang/lib/StaticAnalyzer/Core/RegionStore.cpp

[PATCH] D81254: [analyzer] Produce symbolic values for C-array elements

NoQ added inline comments. Comment at: clang/lib/StaticAnalyzer/Core/RegionStore.cpp:1709 if (!O.getRegion()) -return UnknownVal(); +return svalBuilder.getRegionValueSymbolVal(R); As soon as contents of the array change during analysis, this becomes

[PATCH] D81254: [analyzer] Produce symbolic values for C-array elements

ASDenysPetrov created this revision. ASDenysPetrov added reviewers: dcoughlin, NoQ, alexfh. ASDenysPetrov added a project: clang. Herald added subscribers: cfe-commits, martong, Charusso, dkrupp, donat.nagy, Szelethus, mikhail.ramalho, a.sidorin, szepet, baloghadamsoftware, xazax.hun. Problem: