[PATCH] D35109: [Analyzer] SValBuilder Comparison Rearrangement

[Balogh, Ádám via Phabricator via cfe-commits]

baloghadamsoftware created this revision.

Since the range-based constraint manager (default) is weak in handling comparisons where symbols are on both sides it is wise to rearrange them to have symbols only on the left side. Thus e.g. `A + n >= B + m` becomes `A - B >= m - n` which enables the constraint manager to store a range `m - n .. MAX_VALUE` for the symbolic expression `A - B`. This can be used later to check whether e.g. `A + k == B + l` can be true, which is also rearranged to `A - B == l - k` so the constraint manager can check whether `l - k` is in the range (thus greater than or equal to `m - m`).


https://reviews.llvm.org/D35109

Files:
  lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp
  test/Analysis/std-c-library-functions.c
  test/Analysis/svalbuilder-rearrange-comparisons.c

-------------- next part --------------
A non-text attachment was scrubbed...
Name: D35109.105589.patch
Type: text/x-patch
Size: 9821 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20170707/a038ea5c/attachment.bin>