Currently pancake FFI functions are all of the form @func(x1, y1, x2, y2) and they extend to C FFI functions as void ffifunc(unsigned char *c, long clen, unsigned char *a, long alen).
FFI functions can technically modify the heap under addresses c and a, but the current pancake driver code is only using it to interface with seL4 Microkit.
So probably for now it should be sufficient to have them as something like:
Currently pancake FFI functions are all of the form
@func(x1, y1, x2, y2)and they extend to C FFI functions asvoid ffifunc(unsigned char *c, long clen, unsigned char *a, long alen). FFI functions can technically modify the heap under addressescanda, but the current pancake driver code is only using it to interface with seL4 Microkit. So probably for now it should be sufficient to have them as something like: