[PATCH] D90157: [analyzer] Rework SValBuilder::evalCast function into maintainable and clear way

[Denys Petrov via Phabricator via cfe-commits]

ASDenysPetrov added a comment.

Who can confirm if this is correct or somewhere it needs fixes? Here is a generated result of `evalCast` from the origin branch(before the patch):

  void foo(int* x,  // &SymRegion{reg_$0<int * x>}
           int** y, // &SymRegion{reg_$0<int ** y>}
           int***z) // &SymRegion{reg_$0<int *** z>}
  {
   (void*)x;    // &SymRegion{reg_$0<int * x>}
   (void*)y;    // &SymRegion{reg_$0<int ** y>}
   (void*)z;    // &SymRegion{reg_$0<int *** z>}
   (void**)x;   // &Element{SymRegion{reg_$0<int * x>},0 S64b,void *}
   (void**)y;   // &SymRegion{reg_$0<int ** y>}
   (void**)z;   // &SymRegion{reg_$2<int *** z>}
   (void***)x;  // &Element{SymRegion{reg_$0<int * x>},0 S64b,void **}
   (void***)y;  // &Element{SymRegion{reg_$1<int ** y>},0 S64b,void **}
   (void***)z;  // &SymRegion{reg_$2<int *** z>}
   (void****)x; // &Element{SymRegion{reg_$0<int * x>},0 S64b,void ***}
   (void****)y; // &Element{SymRegion{reg_$1<int ** y>},0 S64b,void ***}
   (void****)z; // &Element{SymRegion{reg_$2<int *** z>},0 S64b,void ***}
  }

@martong

> https://en.cppreference.com/w/cpp/language/explicit_cast
> https://en.cppreference.com/w/cpp/language/implicit_conversion

Thanks for the links.
@steakhal

> By the same token, I think you should run the test-suite using the Z3 refutation and/or Z3 constraint solver to check if this introduces any regression.

Never worked with Z3 before. I'll try.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D90157