[cfe-dev] [Analyzer][RFC] Function Summaries
Mikhail Ramalho via cfe-dev
cfe-dev at lists.llvm.org
Mon Feb 10 09:15:40 PST 2020
> If we want to pursue Z3 for summaries we first will need to fix some of
> the bugs we currently have. Unfortunately, those are not trivial. So I
> think if this is our goal the first step is to make Z3 support solid.
The biggest issue when encoding the program in SMT is the lack of
extension/truncation in the constraints from the analyzer. The analyzer
drops all casts and the backend has to apply them before encoding including
things like integer promotion; there is even some duplicated code from sema
If you are really interested in using the Z3 backend, my suggestion is to
first support extension/truncation in the analyzer. I might be able to
provide some help there as well.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the cfe-dev