-
I've hidden the nasty bits of the trampoline code as much as I can for now behind some macros, defined in include/lcd-domains/trampoline.h and trampoline_link.h. I updated the glue code example. Everything is working. Hopefully this should make trampolines easier to write, generate, and eventually verify (the macros I wrote will "expand" to some kind of models when we verify).
65db6aff