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
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

Reply via email to