[PATCH] D95799: [analyzer] Symbolicate float values with integral casting

Artem Dergachev via Phabricator via cfe-commits cfe-commits at lists.llvm.org
Wed Mar 3 17:55:01 PST 2021


NoQ added a comment.

> tiny patch

IIUC this is roughly the first time ever when `SValBuilder` starts emitting symbols of float type. This is a huge change with an almost unlimited scope of unexpected side effects and very rigorous testing is required to understand the actual effect of this patch on programs that use floats. I think that generally some symbols are always better than no symbols, even if the constraint manager is completely unable to handle them. But we have to make sure that the entirety of `SValBuilder` and the entirety of `RegionStore` (and possibly the entirety of `ExprEngine`) are ready to deal with completely new kinds of values that they've never seen before.



================
Comment at: clang/test/Analysis/svalbuilder-float-cast.c:11
   *p += 1;
-  // This should NOT be (float)$x + 1. Symbol $x was never casted to float.
-  // FIXME: Ideally, this should be $x + 1.
----------------
You silently ignored and removed this comment. The author of the original code was pretty certain that your solution is incorrect and most likely added this comment there specifically to make sure your solution doesn't get implemented.

If you see potential problems with your patch, please don't try to sweep them under the rug. If you're sure your solution is correct, please explain why. If not, please ask about it in the summary or in the comments.

Generally, every commit should be obvious. If there are obvious questions that remain unanswered then the commit is not obvious and needs improvement.


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

https://reviews.llvm.org/D95799



More information about the cfe-commits mailing list