[PATCH] D110913: [analyzer][solver] Handle simplification to ConcreteInt

[Balázs Benics via Phabricator via cfe-commits]

steakhal added a comment.

The patch seems reasonable, but I will need slightly more time to digest it.
I'll get back to this.



================
Comment at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h:390-396
 /// Try to simplify a given symbolic expression's associated value based on the
 /// constraints in State. This is needed because the Environment bindings are
 /// not getting updated when a new constraint is added to the State.
+SVal simplifyToSVal(ProgramStateRef State, SymbolRef Sym);
+/// If the symbol is simplified to a constant then it returns the original
+/// symbol.
 SymbolRef simplify(ProgramStateRef State, SymbolRef Sym);
----------------
I'm confused about which comment corresponds to which function.
You should also signify the difference between the two APIs.

Shouldn't be one of them an implementation detail? If so, why do we have the same visibility?


================
Comment at: clang/test/Analysis/solver-sym-simplification-concreteint.c:22
+  // c == 0 --> 0 + 1 == 0 contradiction
+  clang_analyzer_eval(c == 0);    // expected-warning{{FALSE}}
+
----------------
Could we have an `eval(c == -1) // TRUE`?
Also, please disable eager bifurcation to prevent state-splits in the eval arguments.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D110913