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

[Denys Petrov via Phabricator via cfe-commits]

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];
  
    // In reality we don't know but after your patch
    // we're confident that this is "TRUE".
    clang_analyzer_eval(x == y);
  }

I worked on the second case. I found some possible way to resovle it:

  void foo(int *a); // Potentially modifies elements of 'a'.
  void fooRef(int *&a); // Potentially modifies elements of 'a'.
  
  void test2(int *a) {
    // a - &SymRegion{reg_$6<int * a>}
    foo(a); // after this, CSA doesn't change a.
    // a - &SymRegion{reg_$6<int * a>}
    fooRef(a); // after this, CSA changes a.
    // a - &SymRegion{conj_$10{int *, LC1, S925, #1}}
  }

Here we need to make `foo` behave the same as `fooRef`. What do you think?


CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D81254/new/

https://reviews.llvm.org/D81254