Charlie Jacobsen authored Nov 16, 2015 and Vikram Narayanan committed Oct 26, 2016

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).