Xazax-hun wrote: > Yes, significantly faster, and fewer SAT solver timeouts.
The Clang Static Analyzer is going one step further. It is pruning the analysis state really aggressively, it is relying on liveness analysis, and whenever the value of a variable is dead (would not be read in future program points), the corresponding symbols will be pruned from the state. For the really deep path sensitive analysis the CSA is doing, it was really beneficial performance-wise. On the other hand, this approach definitely introduced complexity. The CSA is basically doing garbage collection to figure out what part of the program state is unreachable (e.g., can we read a value through some pointers?). Moreover, actually pruning the analysis state is tricky. If we had `x < y` and `y < z` in our constraints, to correctly prune `y`, we would need to have a new set of constraints like `x+1 < z`. Simply dropping everything with `y` would lose information. https://github.com/llvm/llvm-project/pull/82611 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
