#include "pcie40_driverlib.h" #include <stdio.h> int p40_get_devname(int dev, const char* suffix, char *dst, size_t dstlen) { return snprintf(dst, dstlen, "/dev/pcie40_%d_%s", dev, suffix); }