* to a buffer at <p>, had it been infinitely big.
  */
 static inline int
-VBUSCHANNEL_sanitize_buffer(char *p, int remain, char __iomem *src, int srcmax)
+vbuschannel_sanitize_buffer(char *p, int remain, char __iomem *src, int srcmax)
 {
        int chars = 0;
        int nonprintable_streak = 0;
  * an environment-independent way (since we are in a common header file).
  */
 static inline int
-VBUSCHANNEL_itoa(char *p, int remain, int num)
+vbuschannel_itoa(char *p, int remain, int num)
 {
        int digits = 0;
        char s[32];
  * Returns the number of bytes written to <p>.
  */
 static inline int
-VBUSCHANNEL_devInfoToStringBuffer(ULTRA_VBUS_DEVICEINFO __iomem *devInfo,
+vbuschannel_devinfo_to_string(ULTRA_VBUS_DEVICEINFO __iomem *devinfo,
                                  char *p, int remain, int devix)
 {
        char __iomem *psrc;
        int nsrc, x, i, pad;
        int chars = 0;
 
-       psrc = &(devInfo->devType[0]);
-       nsrc = sizeof(devInfo->devType);
-       if (VBUSCHANNEL_sanitize_buffer(NULL, 0, psrc, nsrc) <= 0)
+       psrc = &(devinfo->devType[0]);
+       nsrc = sizeof(devinfo->devType);
+       if (vbuschannel_sanitize_buffer(NULL, 0, psrc, nsrc) <= 0)
                return 0;
 
        /* emit device index */
        if (devix >= 0) {
                VBUSCHANNEL_ADDACHAR('[', p, remain, chars);
-               x = VBUSCHANNEL_itoa(p, remain, devix);
+               x = vbuschannel_itoa(p, remain, devix);
                p += x;
                remain -= x;
                chars += x;
        }
 
        /* emit device type */
-       x = VBUSCHANNEL_sanitize_buffer(p, remain, psrc, nsrc);
+       x = vbuschannel_sanitize_buffer(p, remain, psrc, nsrc);
        p += x;
        remain -= x;
        chars += x;
        VBUSCHANNEL_ADDACHAR(' ', p, remain, chars);
 
        /* emit driver name */
-       psrc = &(devInfo->drvName[0]);
-       nsrc = sizeof(devInfo->drvName);
-       x = VBUSCHANNEL_sanitize_buffer(p, remain, psrc, nsrc);
+       psrc = &(devinfo->drvName[0]);
+       nsrc = sizeof(devinfo->drvName);
+       x = vbuschannel_sanitize_buffer(p, remain, psrc, nsrc);
        p += x;
        remain -= x;
        chars += x;
        VBUSCHANNEL_ADDACHAR(' ', p, remain, chars);
 
        /* emit strings */
-       psrc = &(devInfo->infoStrings[0]);
-       nsrc = sizeof(devInfo->infoStrings);
-       x = VBUSCHANNEL_sanitize_buffer(p, remain, psrc, nsrc);
+       psrc = &(devinfo->infoStrings[0]);
+       nsrc = sizeof(devinfo->infoStrings);
+       x = vbuschannel_sanitize_buffer(p, remain, psrc, nsrc);
        p += x;
        remain -= x;
        chars += x;