ddcc added a comment.
> For such test cases i'd consider something like this:
>
> // RUN: ... -analyzer-constraints=range -DRANGE ...
> // RUN: ... -analyzer-constraints=z3 ...
>
> #ifdef RANGE
> foo(); // expected-warning{{}}
> #else
> foo(); // no-warning
> #endif
Would this be assuming that the test setup has Z3 installed and both constraint
managers available? I see that `llvm-lit` supports a `REQUIRES` directive, but
I don't know if that can be scoped to just one `RUN`.
> Yep, the analyzer core has a lot of code that says "we denote this value with
> an incorrect symbol here, because even if we provided the correct symbol it
> would be too hard for the RangeConstraintManager to understand". The most
> obvious place is the integral cast code, which leaves the symbol intact
> *most* of the time (all the time until recently).
>
> I think the right way to address these issues is introduce an API in the base
> ConstraintManager interface to ask the solver if he implements a certain
> feature or is capable of dealing with a particular kind of symbol, and change
> our behavior accordingly. We already have one function that was intended to
> do something like this - `ConstraintManager::canReasonAbout()`; not sure if
> it's working or broken.
`canReasonAbout()` works fine, but in its current form, requires parsing each
constraint to determine whether its supported or not. In
https://reviews.llvm.org/D26061, I've pushed the implementation from
SimpleConstraintManager into RangeConstraintManager itself, since
Z3ConstraintManager will also inherit from SimpleConstraintManager but with a
different feature set. However, even with these changes, `canReasonAbout()` is
only called from within SimpleConstraintManager; the feedback doesn't go all
the way back to e.g. SimpleSValBuilder to dynamically change the constraint
complexity at runtime.
https://reviews.llvm.org/D28952
_______________________________________________
cfe-commits mailing list
[email protected]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
