In conclusion (part 2)
Typed Memory Model turns out to be restrictive.
No support for malloc.
Not good at bitwise ops (can Z3 help?).
Cannot parse some non-standard
__attribute__
s (glib).
Lacks some
__builtin_*
functions.