[cfe-dev] [GSoC] Proposal draft

[George Karpenkov via cfe-dev]

Hi Réka,

Looks good overall!

There are two more items which could be included as super-stretch-goals: they would be very important for adoption of the project,
but fall far out of scope of the GSoC:

1) Packaging. This would be a huge barrier for adopting any Z3 work by existing analyzer users,
but maybe we can think about a few vectors where we could make the adoption easier.
E.g. how difficult would it be to add a dependency from the Debian package? Or from homebrew?

2) Stability. Z3 can segfault, bringing the entire analysis down.
The only way to address this I can think of would be running the solver out-of-process, communicating e.g. via SMT-LIB.
But that would considerably complicate the architecture and debugging, and I’m not sure the trade-offs are worth it.

George

> On Mar 26, 2018, at 8:05 AM, Réka Nikolett Kovács <rekanikolett at gmail.com> wrote:
> 
> Hi George and Artem,
> 
> Thanks for all your valuable comments!
> I'll try to address all of them in a couple of hours.
> 
> Réka
> 
> 
> 
> 2018-03-25 22:26 GMT+02:00 George Karpenkov <ekarpenkov at apple.com <mailto: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 <mailto: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 <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/02058fdc/attachment.html>