[GSoC] Proposal draft

Clang Frontend
#1

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

#2

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