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.