[cfe-dev] [GSoC] Proposal draft

Réka Nikolett Kovács via cfe-dev cfe-dev at lists.llvm.org
Mon Mar 26 14:05:41 PDT 2018


Hi,

Thanks again for the comments and explanations. I hope I've incorporated
all of your advice, except for this one.

George: I've been thinking about what you wrote ("unifying a place where
the constraints are dropped, and adding a flag guarding that")
and I have to admit that I'm not sure I understand that precisely.

Constraints dropped before being added to the environment should mean that
SValBuilder gave up while trying to construct a specific
symbolic expression from them (returned an UnknownVal), if I understand
correctly. Now, the logic responsible for this seems pretty
much scattered around, so I thought maybe by unifying you mean creating a
function like the constraint managers' canReasonAbout()?
Supposing that building more complex expressions (if such will be added)
might be expensive, something like that could come handy in
controlling the level of detail. Did you mean something like that?

Thanks,
Réka



2018-03-25 22:26 GMT+02:00 George Karpenkov <ekarpenkov at apple.com>:

> Hi Réka,
>
> Great! I think it would be beneficial to add an example where the
> “complex” constraint is dropped before even being added to the environment,
> and add a stretch goal of fixing those (e.g. by unifying a place where the
> constraints are dropped, and adding a flag guarding that).
>
> George
>
>
> On Mar 24, 2018, at 1:52 PM, Réka Nikolett Kovács <rekanikolett at gmail.com>
> wrote:
>
> Hi,
>
> I'd like to add my own version of a Z3 integration proposal draft:
>
> https://docs.google.com/document/d/1Qpw_rQ8-JFJJtqyJz8YBqui-
> FNcBgJJvpLBvPcCzHV4/edit?usp=sharing
>
> Any feedback would be much appreciated.
>
> Thanks,
> Réka
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20180326/a9c85a41/attachment.html>


More information about the cfe-dev mailing list