[cfe-dev] [Analyzer][RFC] Function Summaries

[Mikhail Ramalho via cfe-dev]

Hi,


> 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
in smt_conv.h.

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.

-- 

Mikhail Ramalho.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20200210/5512e5af/attachment.html>