[llvm-bugs] [Bug 40145] New: [umbrella] Constraint solver improvements.

[via llvm-bugs]

https://bugs.llvm.org/show_bug.cgi?id=40145

            Bug ID: 40145
           Summary: [umbrella] Constraint solver improvements.
           Product: clang
           Version: trunk
          Hardware: All
                OS: All
            Status: NEW
          Severity: enhancement
          Priority: P
         Component: Static Analyzer
          Assignee: dcoughlin at apple.com
          Reporter: noqnoqneo at gmail.com
                CC: dcoughlin at apple.com, llvm-bugs at lists.llvm.org

I'll dup false positives and false negatives that can be fixed by better
constraint solving to this bug for easier tracking, as an effort to simplify
Bugzilla maintenance and make it more useful.

All of the bugs duped here can be addressed with relative ease by integrating a
third-party SMT solver such as Z3. Most likely every single one of them can be
addressed by improving RangeConstraintManager instead, but addressing a
significant portion of them this way boils down to re-inventing an SMT solver.

In some cases Static Analyzer produces simplified symbolic expressions in order
to make life easier for RangeConstraintManager. One of the most common examples
is the problem of implementing integral casts: they are intentionally incorrect
because otherwise symbolic expressions will be too hard for the
RangeConstraintManager to deal with, resulting in a net increase in false
positives. Such bugs will be duped here as well. Bugs that require other,
unrelated improvements to Static Analyzer (eg., better support for pointer
casts that requires RegionStore re-modeling) will not be duped here.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-bugs/attachments/20181223/95a06dea/attachment.html>