#include "fileio.h" void __attribute__ ((section (".FileIO"))) vx_close() { } void __attribute__ ((section (".FileIO"))) vx_fstat() { } void __attribute__ ((section (".FileIO"))) vx_isatty() { } void __attribute__ ((section (".FileIO"))) vx_read() { } void __attribute__ ((section (".FileIO"))) vx_write() { }