Bug

[В начало]

Ошибка # 94

Показать/спрятать трассу ошибок
Error trace
Function bodies
Blocks
  • Others...
    Function bodies without model function calls
    Initialization function calls
    Initialization function bodies
    Entry point
    Entry point body
    Function calls
    Skipped function calls
    Formal parameter names
    Declarations
    Assumes
    Assume conditions
    Returns
    Return values
    DEG initialization
    DEG function calls
    Model function calls
    Model function bodies
    Model asserts
    Model state changes
    Model function function calls
    Model function function bodies
    Model returns
    Model others
    Identation
    Line numbers
    Expand signs
-entry_point
{
1111 ldv_s_imon_driver_usb_driver = 0;
1101 LDV_IN_INTERRUPT = 1;
1110 ldv_initialize() { /* Function call is skipped due to function is undefined */}
1114 goto ldv_32240;
1114 tmp___0 = nondet_int() { /* Function call is skipped due to function is undefined */}
1114 assume(tmp___0 != 0);
1117 goto ldv_32239;
1115 ldv_32239:;
1118 tmp = nondet_int() { /* Function call is skipped due to function is undefined */}
1118 switch (tmp)
1119 assume(tmp == 0);
1123 assume(ldv_s_imon_driver_usb_driver == 0);
1140 -imon_probe(var_group1, var_imon_probe_12_p1)
{
685 usbdev = (struct usb_device *)0;
686 iface_desc = (struct usb_host_interface *)0;
687 rx_endpoint = (struct usb_endpoint_descriptor *)0;
688 tx_endpoint = (struct usb_endpoint_descriptor *)0;
689 rx_urb = (struct urb *)0;
690 tx_urb = (struct urb *)0;
691 driver = (struct lirc_driver *)0;
692 rbuf = (struct lirc_buffer *)0;
693 dev = &(interface->dev);
695 lirc_minor = 0;
697 retval = -12;
698 display_ep_found = 0;
699 ir_ep_found = 0;
700 vfd_proto_6p = 0;
701 context = (struct imon_context *)0;
706 -ldv_mutex_lock_28(&driver_lock)
{
299 -ldv_mutex_lock_driver_lock(ldv_func_arg1)
{
252 assume(!(ldv_mutex_driver_lock != 1));
254 ldv_mutex_driver_lock = 2;
255 return ;;
}
301 mutex_lock(ldv_func_arg1) { /* Function call is skipped due to function is undefined */}
302 return ;;
}
708 +kzalloc(496UL, 208U)
708 context = (struct imon_context *)tmp;
709 assume(!(((unsigned long)context) == ((unsigned long)((struct imon_context *)0))));
716 tmp___0 = usb_match_id(interface, (const struct usb_device_id *)(&ir_only_list)) { /* Function call is skipped due to function is undefined */}
716 assume(!(((unsigned long)tmp___0) != ((unsigned long)((const struct usb_device_id *)0))));
719 context->display = 1;
721 +interface_to_usbdev(interface)
721 usbdev = usb_get_dev(tmp___1) { /* Function call is skipped due to function is undefined */}
722 iface_desc = interface->cur_altsetting;
723 num_endpts = (int)(iface_desc->desc.bNumEndpoints);
724 ifnum = (int)(iface_desc->desc.bInterfaceNumber);
725 vendor = usbdev->descriptor.idVendor;
726 product = usbdev->descriptor.idProduct;
728 descriptor.modname = "lirc_imon";
728 descriptor.function = "imon_probe";
728 descriptor.filename = "/work/ldvuser/ref_launch/work/current--X--drivers--X--defaultlinux-4.3-rc1.tar.xz--X--32_7a--X--cpachecker/linux-4.3-rc1.tar.xz/csd_deg_dscv/7460/dscv_tempdir/dscv/ri/32_7a/drivers/staging/media/lirc/lirc_imon.c";
728 descriptor.format = "%s: found iMON device (%04x:%04x, intf%d)\n";
728 descriptor.lineno = 729U;
728 descriptor.flags = 0U;
728 +__builtin_expect(((long)(descriptor.flags)) & 1L, 0L)
728 assume(!(tmp___2 != 0L));
736 i = 0;
736 goto ldv_32167;
736 assume(i < num_endpts);
736 assume(ir_ep_found == 0);
738 goto ldv_32166;
737 ldv_32166:;
741 ep = &(((iface_desc->endpoint) + ((unsigned long)i))->desc);
742 int __CPAchecker_TMP_0 = (int)(ep->bEndpointAddress);
742 ep_dir = __CPAchecker_TMP_0 & 128;
743 +usb_endpoint_type((const struct usb_endpoint_descriptor *)ep)
745 assume(ir_ep_found == 0);
745 assume(ep_dir == 128);
745 assume(ep_type == 3);
749 rx_endpoint = ep;
750 ir_ep_found = 1;
751 descriptor___0.modname = "lirc_imon";
751 descriptor___0.function = "imon_probe";
751 descriptor___0.filename = "/work/ldvuser/ref_launch/work/current--X--drivers--X--defaultlinux-4.3-rc1.tar.xz--X--32_7a--X--cpachecker/linux-4.3-rc1.tar.xz/csd_deg_dscv/7460/dscv_tempdir/dscv/ri/32_7a/drivers/staging/media/lirc/lirc_imon.c";
751 descriptor___0.format = "%s: found IR endpoint\n";
751 descriptor___0.lineno = 751U;
751 descriptor___0.flags = 0U;
751 +__builtin_expect(((long)(descriptor___0.flags)) & 1L, 0L)
751 assume(!(tmp___3 != 0L));
736 i = i + 1;
737 ldv_32167:;
736 assume(!(i < num_endpts));
766 assume(!((context->display) == 0));
772 assume(!(ir_ep_found == 0));
780 assume(!(display_ep_found != 0));
788 +kzalloc(144UL, 208U)
788 driver = (struct lirc_driver *)tmp___8;
789 assume(!(((unsigned long)driver) == ((unsigned long)((struct lirc_driver *)0))));
792 +kmalloc(192UL, 208U)
792 rbuf = (struct lirc_buffer *)tmp___9;
793 assume(!(((unsigned long)rbuf) == ((unsigned long)((struct lirc_buffer *)0))));
796 +lirc_buffer_init(rbuf, 4U, 128U)
796 assume(!(tmp___10 != 0));
800 rx_urb = usb_alloc_urb(0, 208U) { /* Function call is skipped due to function is undefined */}
801 assume(!(((unsigned long)rx_urb) == ((unsigned long)((struct urb *)0))));
805 tx_urb = usb_alloc_urb(0, 208U) { /* Function call is skipped due to function is undefined */}
806 assume(!(((unsigned long)tx_urb) == ((unsigned long)((struct urb *)0))));
812 __mutex_init(&(context->ctx_lock), "&context->ctx_lock", &__key) { /* Function call is skipped due to function is undefined */}
813 context->vfd_proto_6p = vfd_proto_6p;
815 strcpy((char *)(&(driver->name)), "lirc_imon") { /* Function call is skipped due to function is undefined */}
816 driver->minor = -1;
817 driver->code_length = 32U;
818 driver->sample_rate = 0;
819 driver->features = 262144U;
820 driver->data = (void *)context;
821 driver->rbuf = rbuf;
822 driver->set_use_inc = &ir_open;
823 driver->set_use_dec = &ir_close;
824 driver->dev = &(interface->dev);
825 driver->owner = &__this_module;
827 -ldv_mutex_lock_29(&(context->ctx_lock))
{
307 -ldv_mutex_lock_ctx_lock_of_imon_context(ldv_func_arg1)
{
66 assume(!(ldv_mutex_ctx_lock_of_imon_context != 1));
68 ldv_mutex_ctx_lock_of_imon_context = 2;
69 return ;;
}
309 mutex_lock(ldv_func_arg1) { /* Function call is skipped due to function is undefined */}
310 return ;;
}
829 context->driver = driver;
832 lirc_minor = lirc_register_driver(driver) { /* Function call is skipped due to function is undefined */}
833 assume(!(lirc_minor < 0));
838 _dev_info((const struct device *)dev, "Registered iMON driver (lirc minor: %d)\n", lirc_minor) { /* Function call is skipped due to function is undefined */}
842 driver->minor = lirc_minor;
844 context->usbdev = usbdev;
845 context->dev_present = 1;
846 context->rx_endpoint = rx_endpoint;
847 context->rx_urb = rx_urb;
853 context->tx_endpoint = tx_endpoint;
854 context->tx_urb = tx_urb;
856 assume(!(display_ep_found != 0));
859 unsigned int __CPAchecker_TMP_1 = (unsigned int)(context->rx_endpoint->bEndpointAddress);
859 +__create_pipe(context->usbdev, __CPAchecker_TMP_1)
859 int __CPAchecker_TMP_2 = (int)(context->rx_endpoint->bInterval);
859 +usb_fill_int_urb(context->rx_urb, context->usbdev, tmp___11 | 1073741952U, (void *)(&(context->usb_rx_buf)), 8, &usb_rx_callback, (void *)context, __CPAchecker_TMP_2)
866 retval = usb_submit_urb(context->rx_urb, 208U) { /* Function call is skipped due to function is undefined */}
867 assume(!(retval != 0));
872 +usb_set_intfdata(interface, (void *)context)
874 assume((context->display) != 0);
874 assume(!(ifnum == 0));
885 _dev_info((const struct device *)dev, "iMON device (%04x:%04x, intf%d) on usb<%d:%d> initialized\n", (int)vendor, (int)product, ifnum, usbdev->bus->busnum, usbdev->devnum) { /* Function call is skipped due to function is undefined */}
889 goto driver_unlock;
913 -ldv_mutex_unlock_30(&driver_lock)
{
315 -ldv_mutex_unlock_driver_lock(ldv_func_arg1)
{
341 assume(!(ldv_mutex_driver_lock != 2));
343 ldv_mutex_driver_lock = 1;
344 return ;;
}
317 mutex_unlock(ldv_func_arg1) { /* Function call is skipped due to function is undefined */}
318 return ;;
}
915 return retval;;
}
1141 ldv_check_return_value(res_imon_probe_12) { /* Function call is skipped due to function is undefined */}
1142 ldv_check_return_value_probe(res_imon_probe_12) { /* Function call is skipped due to function is undefined */}
1143 assume(!(res_imon_probe_12 != 0));
1145 ldv_s_imon_driver_usb_driver = ldv_s_imon_driver_usb_driver + 1;
1151 goto ldv_32234;
1241 ldv_32234:;
1242 ldv_32240:;
1114 tmp___0 = nondet_int() { /* Function call is skipped due to function is undefined */}
1114 assume(!(tmp___0 != 0));
1114 assume(ldv_s_imon_driver_usb_driver != 0);
1117 goto ldv_32239;
1115 ldv_32239:;
1118 tmp = nondet_int() { /* Function call is skipped due to function is undefined */}
1118 switch (tmp)
1119 assume(!(tmp == 0));
1152 assume(tmp == 1);
1155 assume(ldv_s_imon_driver_usb_driver == 1);
1172 ldv_handler_precall() { /* Function call is skipped due to function is undefined */}
1173 +imon_suspend(var_group1, var_imon_suspend_14_p1)
1174 ldv_s_imon_driver_usb_driver = ldv_s_imon_driver_usb_driver + 1;
1180 goto ldv_32234;
1241 ldv_32234:;
1242 ldv_32240:;
1114 tmp___0 = nondet_int() { /* Function call is skipped due to function is undefined */}
1114 assume(!(tmp___0 != 0));
1114 assume(ldv_s_imon_driver_usb_driver != 0);
1117 goto ldv_32239;
1115 ldv_32239:;
1118 tmp = nondet_int() { /* Function call is skipped due to function is undefined */}
1118 switch (tmp)
1119 assume(!(tmp == 0));
1152 assume(!(tmp == 1));
1181 assume(tmp == 2);
1184 assume(ldv_s_imon_driver_usb_driver == 2);
1201 ldv_handler_precall() { /* Function call is skipped due to function is undefined */}
1202 +imon_resume(var_group1)
1203 ldv_s_imon_driver_usb_driver = ldv_s_imon_driver_usb_driver + 1;
1209 goto ldv_32234;
1241 ldv_32234:;
1242 ldv_32240:;
1114 tmp___0 = nondet_int() { /* Function call is skipped due to function is undefined */}
1114 assume(!(tmp___0 != 0));
1114 assume(ldv_s_imon_driver_usb_driver != 0);
1117 goto ldv_32239;
1115 ldv_32239:;
1118 tmp = nondet_int() { /* Function call is skipped due to function is undefined */}
1118 switch (tmp)
1119 assume(!(tmp == 0));
1152 assume(!(tmp == 1));
1181 assume(!(tmp == 2));
1210 assume(tmp == 3);
1213 assume(ldv_s_imon_driver_usb_driver == 3);
1230 ldv_handler_precall() { /* Function call is skipped due to function is undefined */}
1231 -imon_disconnect(var_group1)
{
927 -ldv_mutex_lock_31(&driver_lock)
{
323 -ldv_mutex_lock_driver_lock(ldv_func_arg1)
{
252 assume(!(ldv_mutex_driver_lock != 1));
254 ldv_mutex_driver_lock = 2;
255 return ;;
}
325 mutex_lock(ldv_func_arg1) { /* Function call is skipped due to function is undefined */}
326 return ;;
}
929 +usb_get_intfdata(interface)
929 context = (struct imon_context *)tmp;
930 ifnum = (int)(interface->cur_altsetting->desc.bInterfaceNumber);
932 -ldv_mutex_lock_32(&(context->ctx_lock))
{
331 -ldv_mutex_lock_ctx_lock_of_imon_context(ldv_func_arg1)
{
66 assume(ldv_mutex_ctx_lock_of_imon_context != 1);
66 +ldv_error()
}
}
}
}
Source code
1 2 /* 3 * lirc_imon.c: LIRC/VFD/LCD driver for SoundGraph iMON IR/VFD/LCD 4 * including the iMON PAD model 5 * 6 * Copyright(C) 2004 Venky Raju(dev@venky.ws) 7 * Copyright(C) 2009 Jarod Wilson <jarod@wilsonet.com> 8 * 9 * lirc_imon is free software; you can redistribute it and/or modify 10 * it under the terms of the GNU General Public License as published by 11 * the Free Software Foundation; either version 2 of the License, or 12 * (at your option) any later version. 13 * 14 * This program is distributed in the hope that it will be useful, 15 * but WITHOUT ANY WARRANTY; without even the implied warranty of 16 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 17 * GNU General Public License for more details. 18 * 19 * You should have received a copy of the GNU General Public License 20 * along with this program; if not, write to the Free Software 21 * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. 22 */ 23 24 #define pr_fmt(fmt) KBUILD_MODNAME ": " fmt 25 26 #include <linux/errno.h> 27 #include <linux/kernel.h> 28 #include <linux/module.h> 29 #include <linux/slab.h> 30 #include <linux/uaccess.h> 31 #include <linux/usb.h> 32 33 #include <media/lirc.h> 34 #include <media/lirc_dev.h> 35 36 37 #define MOD_AUTHOR "Venky Raju <dev@venky.ws>" 38 #define MOD_DESC "Driver for SoundGraph iMON MultiMedia IR/Display" 39 #define MOD_NAME "lirc_imon" 40 #define MOD_VERSION "0.8" 41 42 #define DISPLAY_MINOR_BASE 144 43 #define DEVICE_NAME "lcd%d" 44 45 #define BUF_CHUNK_SIZE 4 46 #define BUF_SIZE 128 47 48 #define BIT_DURATION 250 /* each bit received is 250us */ 49 50 /*** P R O T O T Y P E S ***/ 51 52 /* USB Callback prototypes */ 53 static int imon_probe(struct usb_interface *interface, 54 const struct usb_device_id *id); 55 static void imon_disconnect(struct usb_interface *interface); 56 static void usb_rx_callback(struct urb *urb); 57 static void usb_tx_callback(struct urb *urb); 58 59 /* suspend/resume support */ 60 static int imon_resume(struct usb_interface *intf); 61 static int imon_suspend(struct usb_interface *intf, pm_message_t message); 62 63 /* Display file_operations function prototypes */ 64 static int display_open(struct inode *inode, struct file *file); 65 static int display_close(struct inode *inode, struct file *file); 66 67 /* VFD write operation */ 68 static ssize_t vfd_write(struct file *file, const char __user *buf, 69 size_t n_bytes, loff_t *pos); 70 71 /* LIRC driver function prototypes */ 72 static int ir_open(void *data); 73 static void ir_close(void *data); 74 75 /*** G L O B A L S ***/ 76 #define IMON_DATA_BUF_SZ 35 77 78 struct imon_context { 79 struct usb_device *usbdev; 80 /* Newer devices have two interfaces */ 81 int display; /* not all controllers do */ 82 int display_isopen; /* display port has been opened */ 83 int ir_isopen; /* IR port open */ 84 int dev_present; /* USB device presence */ 85 struct mutex ctx_lock; /* to lock this object */ 86 wait_queue_head_t remove_ok; /* For unexpected USB disconnects */ 87 88 int vfd_proto_6p; /* some VFD require a 6th packet */ 89 90 struct lirc_driver *driver; 91 struct usb_endpoint_descriptor *rx_endpoint; 92 struct usb_endpoint_descriptor *tx_endpoint; 93 struct urb *rx_urb; 94 struct urb *tx_urb; 95 unsigned char usb_rx_buf[8]; 96 unsigned char usb_tx_buf[8]; 97 98 struct rx_data { 99 int count; /* length of 0 or 1 sequence */ 100 int prev_bit; /* logic level of sequence */ 101 int initial_space; /* initial space flag */ 102 } rx; 103 104 struct tx_t { 105 unsigned char data_buf[IMON_DATA_BUF_SZ]; /* user data buffer */ 106 struct completion finished; /* wait for write to finish */ 107 atomic_t busy; /* write in progress */ 108 int status; /* status of tx completion */ 109 } tx; 110 }; 111 112 static const struct file_operations display_fops = { 113 .owner = THIS_MODULE, 114 .open = &display_open, 115 .write = &vfd_write, 116 .release = &display_close, 117 .llseek = noop_llseek, 118 }; 119 120 /* 121 * USB Device ID for iMON USB Control Boards 122 * 123 * The Windows drivers contain 6 different inf files, more or less one for 124 * each new device until the 0x0034-0x0046 devices, which all use the same 125 * driver. Some of the devices in the 34-46 range haven't been definitively 126 * identified yet. Early devices have either a TriGem Computer, Inc. or a 127 * Samsung vendor ID (0x0aa8 and 0x04e8 respectively), while all later 128 * devices use the SoundGraph vendor ID (0x15c2). 129 */ 130 static struct usb_device_id imon_usb_id_table[] = { 131 /* TriGem iMON (IR only) -- TG_iMON.inf */ 132 { USB_DEVICE(0x0aa8, 0x8001) }, 133 134 /* SoundGraph iMON (IR only) -- sg_imon.inf */ 135 { USB_DEVICE(0x04e8, 0xff30) }, 136 137 /* SoundGraph iMON VFD (IR & VFD) -- iMON_VFD.inf */ 138 { USB_DEVICE(0x0aa8, 0xffda) }, 139 140 /* SoundGraph iMON SS (IR & VFD) -- iMON_SS.inf */ 141 { USB_DEVICE(0x15c2, 0xffda) }, 142 143 {} 144 }; 145 146 /* Some iMON VFD models requires a 6th packet for VFD writes */ 147 static struct usb_device_id vfd_proto_6p_list[] = { 148 { USB_DEVICE(0x15c2, 0xffda) }, 149 {} 150 }; 151 152 /* Some iMON devices have no lcd/vfd, don't set one up */ 153 static struct usb_device_id ir_only_list[] = { 154 { USB_DEVICE(0x0aa8, 0x8001) }, 155 { USB_DEVICE(0x04e8, 0xff30) }, 156 {} 157 }; 158 159 /* USB Device data */ 160 static struct usb_driver imon_driver = { 161 .name = MOD_NAME, 162 .probe = imon_probe, 163 .disconnect = imon_disconnect, 164 .suspend = imon_suspend, 165 .resume = imon_resume, 166 .id_table = imon_usb_id_table, 167 }; 168 169 static struct usb_class_driver imon_class = { 170 .name = DEVICE_NAME, 171 .fops = &display_fops, 172 .minor_base = DISPLAY_MINOR_BASE, 173 }; 174 175 /* to prevent races between open() and disconnect(), probing, etc */ 176 static DEFINE_MUTEX(driver_lock); 177 178 static int debug; 179 180 /*** M O D U L E C O D E ***/ 181 182 MODULE_AUTHOR(MOD_AUTHOR); 183 MODULE_DESCRIPTION(MOD_DESC); 184 MODULE_VERSION(MOD_VERSION); 185 MODULE_LICENSE("GPL"); 186 MODULE_DEVICE_TABLE(usb, imon_usb_id_table); 187 module_param(debug, int, S_IRUGO | S_IWUSR); 188 MODULE_PARM_DESC(debug, "Debug messages: 0=no, 1=yes(default: no)"); 189 190 static void free_imon_context(struct imon_context *context) 191 { 192 struct device *dev = context->driver->dev; 193 194 usb_free_urb(context->tx_urb); 195 usb_free_urb(context->rx_urb); 196 lirc_buffer_free(context->driver->rbuf); 197 kfree(context->driver->rbuf); 198 kfree(context->driver); 199 kfree(context); 200 201 dev_dbg(dev, "%s: iMON context freed\n", __func__); 202 } 203 204 static void deregister_from_lirc(struct imon_context *context) 205 { 206 int retval; 207 int minor = context->driver->minor; 208 209 retval = lirc_unregister_driver(minor); 210 if (retval) 211 dev_err(&context->usbdev->dev, 212 "unable to deregister from lirc(%d)", retval); 213 else 214 dev_info(&context->usbdev->dev, 215 "Deregistered iMON driver (minor:%d)\n", minor); 216 217 } 218 219 /** 220 * Called when the Display device (e.g. /dev/lcd0) 221 * is opened by the application. 222 */ 223 static int display_open(struct inode *inode, struct file *file) 224 { 225 struct usb_interface *interface; 226 struct imon_context *context = NULL; 227 int subminor; 228 int retval = 0; 229 230 /* prevent races with disconnect */ 231 mutex_lock(&driver_lock); 232 233 subminor = iminor(inode); 234 interface = usb_find_interface(&imon_driver, subminor); 235 if (!interface) { 236 pr_err("%s: could not find interface for minor %d\n", 237 __func__, subminor); 238 retval = -ENODEV; 239 goto exit; 240 } 241 context = usb_get_intfdata(interface); 242 243 if (!context) { 244 dev_err(&interface->dev, "no context found for minor %d\n", 245 subminor); 246 retval = -ENODEV; 247 goto exit; 248 } 249 250 mutex_lock(&context->ctx_lock); 251 252 if (!context->display) { 253 dev_err(&interface->dev, 254 "%s: display not supported by device\n", __func__); 255 retval = -ENODEV; 256 } else if (context->display_isopen) { 257 dev_err(&interface->dev, 258 "%s: display port is already open\n", __func__); 259 retval = -EBUSY; 260 } else { 261 context->display_isopen = 1; 262 file->private_data = context; 263 dev_info(context->driver->dev, "display port opened\n"); 264 } 265 266 mutex_unlock(&context->ctx_lock); 267 268 exit: 269 mutex_unlock(&driver_lock); 270 return retval; 271 } 272 273 /** 274 * Called when the display device (e.g. /dev/lcd0) 275 * is closed by the application. 276 */ 277 static int display_close(struct inode *inode, struct file *file) 278 { 279 struct imon_context *context = NULL; 280 int retval = 0; 281 282 context = file->private_data; 283 284 if (!context) { 285 pr_err("%s: no context for device\n", __func__); 286 return -ENODEV; 287 } 288 289 mutex_lock(&context->ctx_lock); 290 291 if (!context->display) { 292 dev_err(&context->usbdev->dev, 293 "%s: display not supported by device\n", __func__); 294 retval = -ENODEV; 295 } else if (!context->display_isopen) { 296 dev_err(&context->usbdev->dev, 297 "%s: display is not open\n", __func__); 298 retval = -EIO; 299 } else { 300 context->display_isopen = 0; 301 dev_info(context->driver->dev, "display port closed\n"); 302 if (!context->dev_present && !context->ir_isopen) { 303 /* 304 * Device disconnected before close and IR port is not 305 * open. If IR port is open, context will be deleted by 306 * ir_close. 307 */ 308 mutex_unlock(&context->ctx_lock); 309 free_imon_context(context); 310 return retval; 311 } 312 } 313 314 mutex_unlock(&context->ctx_lock); 315 return retval; 316 } 317 318 /** 319 * Sends a packet to the device -- this function must be called 320 * with context->ctx_lock held. 321 */ 322 static int send_packet(struct imon_context *context) 323 { 324 unsigned int pipe; 325 int interval = 0; 326 int retval = 0; 327 328 /* Check if we need to use control or interrupt urb */ 329 pipe = usb_sndintpipe(context->usbdev, 330 context->tx_endpoint->bEndpointAddress); 331 interval = context->tx_endpoint->bInterval; 332 333 usb_fill_int_urb(context->tx_urb, context->usbdev, pipe, 334 context->usb_tx_buf, 335 sizeof(context->usb_tx_buf), 336 usb_tx_callback, context, interval); 337 338 context->tx_urb->actual_length = 0; 339 340 init_completion(&context->tx.finished); 341 atomic_set(&context->tx.busy, 1); 342 343 retval = usb_submit_urb(context->tx_urb, GFP_KERNEL); 344 if (retval) { 345 atomic_set(&context->tx.busy, 0); 346 dev_err(&context->usbdev->dev, "error submitting urb(%d)\n", 347 retval); 348 } else { 349 /* Wait for transmission to complete (or abort) */ 350 mutex_unlock(&context->ctx_lock); 351 retval = wait_for_completion_interruptible( 352 &context->tx.finished); 353 if (retval) 354 dev_err(&context->usbdev->dev, 355 "%s: task interrupted\n", __func__); 356 mutex_lock(&context->ctx_lock); 357 358 retval = context->tx.status; 359 if (retval) 360 dev_err(&context->usbdev->dev, 361 "packet tx failed (%d)\n", retval); 362 } 363 364 return retval; 365 } 366 367 /** 368 * Writes data to the VFD. The iMON VFD is 2x16 characters 369 * and requires data in 5 consecutive USB interrupt packets, 370 * each packet but the last carrying 7 bytes. 371 * 372 * I don't know if the VFD board supports features such as 373 * scrolling, clearing rows, blanking, etc. so at 374 * the caller must provide a full screen of data. If fewer 375 * than 32 bytes are provided spaces will be appended to 376 * generate a full screen. 377 */ 378 static ssize_t vfd_write(struct file *file, const char __user *buf, 379 size_t n_bytes, loff_t *pos) 380 { 381 int i; 382 int offset; 383 int seq; 384 int retval = 0; 385 struct imon_context *context; 386 const unsigned char vfd_packet6[] = { 387 0x01, 0x00, 0x00, 0x00, 0x00, 0xFF, 0xFF }; 388 int *data_buf = NULL; 389 390 context = file->private_data; 391 if (!context) { 392 pr_err("%s: no context for device\n", __func__); 393 return -ENODEV; 394 } 395 396 mutex_lock(&context->ctx_lock); 397 398 if (!context->dev_present) { 399 dev_err(&context->usbdev->dev, 400 "%s: no iMON device present\n", __func__); 401 retval = -ENODEV; 402 goto exit; 403 } 404 405 if (n_bytes <= 0 || n_bytes > IMON_DATA_BUF_SZ - 3) { 406 dev_err(&context->usbdev->dev, 407 "%s: invalid payload size\n", __func__); 408 retval = -EINVAL; 409 goto exit; 410 } 411 412 data_buf = memdup_user(buf, n_bytes); 413 if (IS_ERR(data_buf)) { 414 retval = PTR_ERR(data_buf); 415 data_buf = NULL; 416 goto exit; 417 } 418 419 memcpy(context->tx.data_buf, data_buf, n_bytes); 420 421 /* Pad with spaces */ 422 for (i = n_bytes; i < IMON_DATA_BUF_SZ - 3; ++i) 423 context->tx.data_buf[i] = ' '; 424 425 for (i = IMON_DATA_BUF_SZ - 3; i < IMON_DATA_BUF_SZ; ++i) 426 context->tx.data_buf[i] = 0xFF; 427 428 offset = 0; 429 seq = 0; 430 431 do { 432 memcpy(context->usb_tx_buf, context->tx.data_buf + offset, 7); 433 context->usb_tx_buf[7] = (unsigned char) seq; 434 435 retval = send_packet(context); 436 if (retval) { 437 dev_err(&context->usbdev->dev, 438 "send packet failed for packet #%d\n", 439 seq / 2); 440 goto exit; 441 } else { 442 seq += 2; 443 offset += 7; 444 } 445 446 } while (offset < IMON_DATA_BUF_SZ); 447 448 if (context->vfd_proto_6p) { 449 /* Send packet #6 */ 450 memcpy(context->usb_tx_buf, &vfd_packet6, sizeof(vfd_packet6)); 451 context->usb_tx_buf[7] = (unsigned char) seq; 452 retval = send_packet(context); 453 if (retval) 454 dev_err(&context->usbdev->dev, 455 "send packet failed for packet #%d\n", 456 seq / 2); 457 } 458 459 exit: 460 mutex_unlock(&context->ctx_lock); 461 kfree(data_buf); 462 463 return (!retval) ? n_bytes : retval; 464 } 465 466 /** 467 * Callback function for USB core API: transmit data 468 */ 469 static void usb_tx_callback(struct urb *urb) 470 { 471 struct imon_context *context; 472 473 if (!urb) 474 return; 475 context = (struct imon_context *)urb->context; 476 if (!context) 477 return; 478 479 context->tx.status = urb->status; 480 481 /* notify waiters that write has finished */ 482 atomic_set(&context->tx.busy, 0); 483 complete(&context->tx.finished); 484 } 485 486 /** 487 * Called by lirc_dev when the application opens /dev/lirc 488 */ 489 static int ir_open(void *data) 490 { 491 struct imon_context *context; 492 493 /* prevent races with disconnect */ 494 mutex_lock(&driver_lock); 495 496 context = data; 497 498 /* initial IR protocol decode variables */ 499 context->rx.count = 0; 500 context->rx.initial_space = 1; 501 context->rx.prev_bit = 0; 502 503 context->ir_isopen = 1; 504 dev_info(context->driver->dev, "IR port opened\n"); 505 506 mutex_unlock(&driver_lock); 507 return 0; 508 } 509 510 /** 511 * Called by lirc_dev when the application closes /dev/lirc 512 */ 513 static void ir_close(void *data) 514 { 515 struct imon_context *context; 516 517 context = data; 518 if (!context) { 519 pr_err("%s: no context for device\n", __func__); 520 return; 521 } 522 523 mutex_lock(&context->ctx_lock); 524 525 context->ir_isopen = 0; 526 dev_info(context->driver->dev, "IR port closed\n"); 527 528 if (!context->dev_present) { 529 /* 530 * Device disconnected while IR port was still open. Driver 531 * was not deregistered at disconnect time, so do it now. 532 */ 533 deregister_from_lirc(context); 534 535 if (!context->display_isopen) { 536 mutex_unlock(&context->ctx_lock); 537 free_imon_context(context); 538 return; 539 } 540 /* 541 * If display port is open, context will be deleted by 542 * display_close 543 */ 544 } 545 546 mutex_unlock(&context->ctx_lock); 547 } 548 549 /** 550 * Convert bit count to time duration (in us) and submit 551 * the value to lirc_dev. 552 */ 553 static void submit_data(struct imon_context *context) 554 { 555 unsigned char buf[4]; 556 int value = context->rx.count; 557 int i; 558 559 dev_dbg(context->driver->dev, "submitting data to LIRC\n"); 560 561 value *= BIT_DURATION; 562 value &= PULSE_MASK; 563 if (context->rx.prev_bit) 564 value |= PULSE_BIT; 565 566 for (i = 0; i < 4; ++i) 567 buf[i] = value>>(i*8); 568 569 lirc_buffer_write(context->driver->rbuf, buf); 570 wake_up(&context->driver->rbuf->wait_poll); 571 } 572 573 /** 574 * Process the incoming packet 575 */ 576 static void imon_incoming_packet(struct imon_context *context, 577 struct urb *urb, int intf) 578 { 579 int len = urb->actual_length; 580 unsigned char *buf = urb->transfer_buffer; 581 struct device *dev = context->driver->dev; 582 int octet, bit; 583 unsigned char mask; 584 585 /* 586 * just bail out if no listening IR client 587 */ 588 if (!context->ir_isopen) 589 return; 590 591 if (len != 8) { 592 dev_warn(dev, "imon %s: invalid incoming packet size (len = %d, intf%d)\n", 593 __func__, len, intf); 594 return; 595 } 596 597 if (debug) 598 dev_info(dev, "raw packet: %*ph\n", len, buf); 599 /* 600 * Translate received data to pulse and space lengths. 601 * Received data is active low, i.e. pulses are 0 and 602 * spaces are 1. 603 * 604 * My original algorithm was essentially similar to 605 * Changwoo Ryu's with the exception that he switched 606 * the incoming bits to active high and also fed an 607 * initial space to LIRC at the start of a new sequence 608 * if the previous bit was a pulse. 609 * 610 * I've decided to adopt his algorithm. 611 */ 612 613 if (buf[7] == 1 && context->rx.initial_space) { 614 /* LIRC requires a leading space */ 615 context->rx.prev_bit = 0; 616 context->rx.count = 4; 617 submit_data(context); 618 context->rx.count = 0; 619 } 620 621 for (octet = 0; octet < 5; ++octet) { 622 mask = 0x80; 623 for (bit = 0; bit < 8; ++bit) { 624 int curr_bit = !(buf[octet] & mask); 625 626 if (curr_bit != context->rx.prev_bit) { 627 if (context->rx.count) { 628 submit_data(context); 629 context->rx.count = 0; 630 } 631 context->rx.prev_bit = curr_bit; 632 } 633 ++context->rx.count; 634 mask >>= 1; 635 } 636 } 637 638 if (buf[7] == 10) { 639 if (context->rx.count) { 640 submit_data(context); 641 context->rx.count = 0; 642 } 643 context->rx.initial_space = context->rx.prev_bit; 644 } 645 } 646 647 /** 648 * Callback function for USB core API: receive data 649 */ 650 static void usb_rx_callback(struct urb *urb) 651 { 652 struct imon_context *context; 653 int intfnum = 0; 654 655 if (!urb) 656 return; 657 658 context = (struct imon_context *)urb->context; 659 if (!context) 660 return; 661 662 switch (urb->status) { 663 case -ENOENT: /* usbcore unlink successful! */ 664 return; 665 666 case 0: 667 imon_incoming_packet(context, urb, intfnum); 668 break; 669 670 default: 671 dev_warn(context->driver->dev, "imon %s: status(%d): ignored\n", 672 __func__, urb->status); 673 break; 674 } 675 676 usb_submit_urb(context->rx_urb, GFP_ATOMIC); 677 } 678 679 /** 680 * Callback function for USB core API: Probe 681 */ 682 static int imon_probe(struct usb_interface *interface, 683 const struct usb_device_id *id) 684 { 685 struct usb_device *usbdev = NULL; 686 struct usb_host_interface *iface_desc = NULL; 687 struct usb_endpoint_descriptor *rx_endpoint = NULL; 688 struct usb_endpoint_descriptor *tx_endpoint = NULL; 689 struct urb *rx_urb = NULL; 690 struct urb *tx_urb = NULL; 691 struct lirc_driver *driver = NULL; 692 struct lirc_buffer *rbuf = NULL; 693 struct device *dev = &interface->dev; 694 int ifnum; 695 int lirc_minor = 0; 696 int num_endpts; 697 int retval = -ENOMEM; 698 int display_ep_found = 0; 699 int ir_ep_found = 0; 700 int vfd_proto_6p = 0; 701 struct imon_context *context = NULL; 702 int i; 703 u16 vendor, product; 704 705 /* prevent races probing devices w/multiple interfaces */ 706 mutex_lock(&driver_lock); 707 708 context = kzalloc(sizeof(struct imon_context), GFP_KERNEL); 709 if (!context) 710 goto driver_unlock; 711 712 /* 713 * Try to auto-detect the type of display if the user hasn't set 714 * it by hand via the display_type modparam. Default is VFD. 715 */ 716 if (usb_match_id(interface, ir_only_list)) 717 context->display = 0; 718 else 719 context->display = 1; 720 721 usbdev = usb_get_dev(interface_to_usbdev(interface)); 722 iface_desc = interface->cur_altsetting; 723 num_endpts = iface_desc->desc.bNumEndpoints; 724 ifnum = iface_desc->desc.bInterfaceNumber; 725 vendor = le16_to_cpu(usbdev->descriptor.idVendor); 726 product = le16_to_cpu(usbdev->descriptor.idProduct); 727 728 dev_dbg(dev, "%s: found iMON device (%04x:%04x, intf%d)\n", 729 __func__, vendor, product, ifnum); 730 731 /* 732 * Scan the endpoint list and set: 733 * first input endpoint = IR endpoint 734 * first output endpoint = display endpoint 735 */ 736 for (i = 0; i < num_endpts && !(ir_ep_found && display_ep_found); ++i) { 737 struct usb_endpoint_descriptor *ep; 738 int ep_dir; 739 int ep_type; 740 741 ep = &iface_desc->endpoint[i].desc; 742 ep_dir = ep->bEndpointAddress & USB_ENDPOINT_DIR_MASK; 743 ep_type = usb_endpoint_type(ep); 744 745 if (!ir_ep_found && 746 ep_dir == USB_DIR_IN && 747 ep_type == USB_ENDPOINT_XFER_INT) { 748 749 rx_endpoint = ep; 750 ir_ep_found = 1; 751 dev_dbg(dev, "%s: found IR endpoint\n", __func__); 752 753 } else if (!display_ep_found && ep_dir == USB_DIR_OUT && 754 ep_type == USB_ENDPOINT_XFER_INT) { 755 tx_endpoint = ep; 756 display_ep_found = 1; 757 dev_dbg(dev, "%s: found display endpoint\n", __func__); 758 } 759 } 760 761 /* 762 * Some iMON receivers have no display. Unfortunately, it seems 763 * that SoundGraph recycles device IDs between devices both with 764 * and without... :\ 765 */ 766 if (context->display == 0) { 767 display_ep_found = 0; 768 dev_dbg(dev, "%s: device has no display\n", __func__); 769 } 770 771 /* Input endpoint is mandatory */ 772 if (!ir_ep_found) { 773 dev_err(dev, "%s: no valid input (IR) endpoint found.\n", 774 __func__); 775 retval = -ENODEV; 776 goto free_context; 777 } 778 779 /* Determine if display requires 6 packets */ 780 if (display_ep_found) { 781 if (usb_match_id(interface, vfd_proto_6p_list)) 782 vfd_proto_6p = 1; 783 784 dev_dbg(dev, "%s: vfd_proto_6p: %d\n", 785 __func__, vfd_proto_6p); 786 } 787 788 driver = kzalloc(sizeof(struct lirc_driver), GFP_KERNEL); 789 if (!driver) 790 goto free_context; 791 792 rbuf = kmalloc(sizeof(struct lirc_buffer), GFP_KERNEL); 793 if (!rbuf) 794 goto free_driver; 795 796 if (lirc_buffer_init(rbuf, BUF_CHUNK_SIZE, BUF_SIZE)) { 797 dev_err(dev, "%s: lirc_buffer_init failed\n", __func__); 798 goto free_rbuf; 799 } 800 rx_urb = usb_alloc_urb(0, GFP_KERNEL); 801 if (!rx_urb) { 802 dev_err(dev, "%s: usb_alloc_urb failed for IR urb\n", __func__); 803 goto free_lirc_buf; 804 } 805 tx_urb = usb_alloc_urb(0, GFP_KERNEL); 806 if (!tx_urb) { 807 dev_err(dev, "%s: usb_alloc_urb failed for display urb\n", 808 __func__); 809 goto free_rx_urb; 810 } 811 812 mutex_init(&context->ctx_lock); 813 context->vfd_proto_6p = vfd_proto_6p; 814 815 strcpy(driver->name, MOD_NAME); 816 driver->minor = -1; 817 driver->code_length = BUF_CHUNK_SIZE * 8; 818 driver->sample_rate = 0; 819 driver->features = LIRC_CAN_REC_MODE2; 820 driver->data = context; 821 driver->rbuf = rbuf; 822 driver->set_use_inc = ir_open; 823 driver->set_use_dec = ir_close; 824 driver->dev = &interface->dev; 825 driver->owner = THIS_MODULE; 826 827 mutex_lock(&context->ctx_lock); 828 829 context->driver = driver; 830 /* start out in keyboard mode */ 831 832 lirc_minor = lirc_register_driver(driver); 833 if (lirc_minor < 0) { 834 dev_err(dev, "%s: lirc_register_driver failed\n", __func__); 835 goto free_tx_urb; 836 } 837 838 dev_info(dev, "Registered iMON driver (lirc minor: %d)\n", 839 lirc_minor); 840 841 /* Needed while unregistering! */ 842 driver->minor = lirc_minor; 843 844 context->usbdev = usbdev; 845 context->dev_present = 1; 846 context->rx_endpoint = rx_endpoint; 847 context->rx_urb = rx_urb; 848 849 /* 850 * tx is used to send characters to lcd/vfd, associate RF 851 * remotes, set IR protocol, and maybe more... 852 */ 853 context->tx_endpoint = tx_endpoint; 854 context->tx_urb = tx_urb; 855 856 if (display_ep_found) 857 context->display = 1; 858 859 usb_fill_int_urb(context->rx_urb, context->usbdev, 860 usb_rcvintpipe(context->usbdev, 861 context->rx_endpoint->bEndpointAddress), 862 context->usb_rx_buf, sizeof(context->usb_rx_buf), 863 usb_rx_callback, context, 864 context->rx_endpoint->bInterval); 865 866 retval = usb_submit_urb(context->rx_urb, GFP_KERNEL); 867 if (retval) { 868 dev_err(dev, "usb_submit_urb failed for intf0 (%d)\n", retval); 869 goto unregister_lirc; 870 } 871 872 usb_set_intfdata(interface, context); 873 874 if (context->display && ifnum == 0) { 875 dev_dbg(dev, "%s: Registering iMON display with sysfs\n", 876 __func__); 877 878 if (usb_register_dev(interface, &imon_class)) { 879 /* Not a fatal error, so ignore */ 880 dev_info(dev, "%s: could not get a minor number for display\n", 881 __func__); 882 } 883 } 884 885 dev_info(dev, "iMON device (%04x:%04x, intf%d) on usb<%d:%d> initialized\n", 886 vendor, product, ifnum, usbdev->bus->busnum, usbdev->devnum); 887 888 /* Everything went fine. Just unlock and return retval (with is 0) */ 889 goto driver_unlock; 890 891 unregister_lirc: 892 lirc_unregister_driver(driver->minor); 893 894 free_tx_urb: 895 usb_free_urb(tx_urb); 896 897 free_rx_urb: 898 usb_free_urb(rx_urb); 899 900 free_lirc_buf: 901 lirc_buffer_free(rbuf); 902 903 free_rbuf: 904 kfree(rbuf); 905 906 free_driver: 907 kfree(driver); 908 free_context: 909 kfree(context); 910 context = NULL; 911 912 driver_unlock: 913 mutex_unlock(&driver_lock); 914 915 return retval; 916 } 917 918 /** 919 * Callback function for USB core API: disconnect 920 */ 921 static void imon_disconnect(struct usb_interface *interface) 922 { 923 struct imon_context *context; 924 int ifnum; 925 926 /* prevent races with ir_open()/display_open() */ 927 mutex_lock(&driver_lock); 928 929 context = usb_get_intfdata(interface); 930 ifnum = interface->cur_altsetting->desc.bInterfaceNumber; 931 932 mutex_lock(&context->ctx_lock); 933 934 usb_set_intfdata(interface, NULL); 935 936 /* Abort ongoing write */ 937 if (atomic_read(&context->tx.busy)) { 938 usb_kill_urb(context->tx_urb); 939 complete_all(&context->tx.finished); 940 } 941 942 context->dev_present = 0; 943 usb_kill_urb(context->rx_urb); 944 if (context->display) 945 usb_deregister_dev(interface, &imon_class); 946 947 if (!context->ir_isopen && !context->dev_present) { 948 deregister_from_lirc(context); 949 mutex_unlock(&context->ctx_lock); 950 if (!context->display_isopen) 951 free_imon_context(context); 952 } else 953 mutex_unlock(&context->ctx_lock); 954 955 mutex_unlock(&driver_lock); 956 957 dev_info(&interface->dev, "%s: iMON device (intf%d) disconnected\n", 958 __func__, ifnum); 959 } 960 961 static int imon_suspend(struct usb_interface *intf, pm_message_t message) 962 { 963 struct imon_context *context = usb_get_intfdata(intf); 964 965 usb_kill_urb(context->rx_urb); 966 967 return 0; 968 } 969 970 static int imon_resume(struct usb_interface *intf) 971 { 972 struct imon_context *context = usb_get_intfdata(intf); 973 974 usb_fill_int_urb(context->rx_urb, context->usbdev, 975 usb_rcvintpipe(context->usbdev, 976 context->rx_endpoint->bEndpointAddress), 977 context->usb_rx_buf, sizeof(context->usb_rx_buf), 978 usb_rx_callback, context, 979 context->rx_endpoint->bInterval); 980 981 return usb_submit_urb(context->rx_urb, GFP_ATOMIC); 982 } 983 984 module_usb_driver(imon_driver); 985 986 987 988 989 990 /* LDV_COMMENT_BEGIN_MAIN */ 991 #ifdef LDV_MAIN0_sequence_infinite_withcheck_stateful 992 993 /*###########################################################################*/ 994 995 /*############## Driver Environment Generator 0.2 output ####################*/ 996 997 /*###########################################################################*/ 998 999 1000 1001 /* LDV_COMMENT_FUNCTION_DECLARE_LDV Special function for LDV verifier. Test if all kernel resources are correctly released by driver before driver will be unloaded. */ 1002 void ldv_check_final_state(void); 1003 1004 /* LDV_COMMENT_FUNCTION_DECLARE_LDV Special function for LDV verifier. Test correct return result. */ 1005 void ldv_check_return_value(int res); 1006 1007 /* LDV_COMMENT_FUNCTION_DECLARE_LDV Special function for LDV verifier. Test correct return result of probe() function. */ 1008 void ldv_check_return_value_probe(int res); 1009 1010 /* LDV_COMMENT_FUNCTION_DECLARE_LDV Special function for LDV verifier. Initializes the model. */ 1011 void ldv_initialize(void); 1012 1013 /* LDV_COMMENT_FUNCTION_DECLARE_LDV Special function for LDV verifier. Reinitializes the model between distinct model function calls. */ 1014 void ldv_handler_precall(void); 1015 1016 /* LDV_COMMENT_FUNCTION_DECLARE_LDV Special function for LDV verifier. Returns arbitrary interger value. */ 1017 int nondet_int(void); 1018 1019 /* LDV_COMMENT_VAR_DECLARE_LDV Special variable for LDV verifier. */ 1020 int LDV_IN_INTERRUPT; 1021 1022 /* LDV_COMMENT_FUNCTION_MAIN Main function for LDV verifier. */ 1023 void ldv_main0_sequence_infinite_withcheck_stateful(void) { 1024 1025 1026 1027 /* LDV_COMMENT_BEGIN_VARIABLE_DECLARATION_PART */ 1028 /*============================= VARIABLE DECLARATION PART =============================*/ 1029 /** STRUCT: struct type: usb_driver, struct name: imon_driver **/ 1030 /* content: static int imon_probe(struct usb_interface *interface, const struct usb_device_id *id)*/ 1031 /* LDV_COMMENT_BEGIN_PREP */ 1032 #define pr_fmt(fmt) KBUILD_MODNAME ": " fmt 1033 #define MOD_AUTHOR "Venky Raju <dev@venky.ws>" 1034 #define MOD_DESC "Driver for SoundGraph iMON MultiMedia IR/Display" 1035 #define MOD_NAME "lirc_imon" 1036 #define MOD_VERSION "0.8" 1037 #define DISPLAY_MINOR_BASE 144 1038 #define DEVICE_NAME "lcd%d" 1039 #define BUF_CHUNK_SIZE 4 1040 #define BUF_SIZE 128 1041 #define BIT_DURATION 250 1042 #define IMON_DATA_BUF_SZ 35 1043 /* LDV_COMMENT_END_PREP */ 1044 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "imon_probe" */ 1045 struct usb_interface * var_group1; 1046 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "imon_probe" */ 1047 const struct usb_device_id * var_imon_probe_12_p1; 1048 /* LDV_COMMENT_VAR_DECLARE Variable declaration for test return result from function call "imon_probe" */ 1049 static int res_imon_probe_12; 1050 /* content: static void imon_disconnect(struct usb_interface *interface)*/ 1051 /* LDV_COMMENT_BEGIN_PREP */ 1052 #define pr_fmt(fmt) KBUILD_MODNAME ": " fmt 1053 #define MOD_AUTHOR "Venky Raju <dev@venky.ws>" 1054 #define MOD_DESC "Driver for SoundGraph iMON MultiMedia IR/Display" 1055 #define MOD_NAME "lirc_imon" 1056 #define MOD_VERSION "0.8" 1057 #define DISPLAY_MINOR_BASE 144 1058 #define DEVICE_NAME "lcd%d" 1059 #define BUF_CHUNK_SIZE 4 1060 #define BUF_SIZE 128 1061 #define BIT_DURATION 250 1062 #define IMON_DATA_BUF_SZ 35 1063 /* LDV_COMMENT_END_PREP */ 1064 /* content: static int imon_suspend(struct usb_interface *intf, pm_message_t message)*/ 1065 /* LDV_COMMENT_BEGIN_PREP */ 1066 #define pr_fmt(fmt) KBUILD_MODNAME ": " fmt 1067 #define MOD_AUTHOR "Venky Raju <dev@venky.ws>" 1068 #define MOD_DESC "Driver for SoundGraph iMON MultiMedia IR/Display" 1069 #define MOD_NAME "lirc_imon" 1070 #define MOD_VERSION "0.8" 1071 #define DISPLAY_MINOR_BASE 144 1072 #define DEVICE_NAME "lcd%d" 1073 #define BUF_CHUNK_SIZE 4 1074 #define BUF_SIZE 128 1075 #define BIT_DURATION 250 1076 #define IMON_DATA_BUF_SZ 35 1077 /* LDV_COMMENT_END_PREP */ 1078 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "imon_suspend" */ 1079 pm_message_t var_imon_suspend_14_p1; 1080 /* content: static int imon_resume(struct usb_interface *intf)*/ 1081 /* LDV_COMMENT_BEGIN_PREP */ 1082 #define pr_fmt(fmt) KBUILD_MODNAME ": " fmt 1083 #define MOD_AUTHOR "Venky Raju <dev@venky.ws>" 1084 #define MOD_DESC "Driver for SoundGraph iMON MultiMedia IR/Display" 1085 #define MOD_NAME "lirc_imon" 1086 #define MOD_VERSION "0.8" 1087 #define DISPLAY_MINOR_BASE 144 1088 #define DEVICE_NAME "lcd%d" 1089 #define BUF_CHUNK_SIZE 4 1090 #define BUF_SIZE 128 1091 #define BIT_DURATION 250 1092 #define IMON_DATA_BUF_SZ 35 1093 /* LDV_COMMENT_END_PREP */ 1094 1095 1096 1097 1098 /* LDV_COMMENT_END_VARIABLE_DECLARATION_PART */ 1099 /* LDV_COMMENT_BEGIN_VARIABLE_INITIALIZING_PART */ 1100 /*============================= VARIABLE INITIALIZING PART =============================*/ 1101 LDV_IN_INTERRUPT=1; 1102 1103 1104 1105 1106 /* LDV_COMMENT_END_VARIABLE_INITIALIZING_PART */ 1107 /* LDV_COMMENT_BEGIN_FUNCTION_CALL_SECTION */ 1108 /*============================= FUNCTION CALL SECTION =============================*/ 1109 /* LDV_COMMENT_FUNCTION_CALL Initialize LDV model. */ 1110 ldv_initialize(); 1111 int ldv_s_imon_driver_usb_driver = 0; 1112 1113 1114 while( nondet_int() 1115 || !(ldv_s_imon_driver_usb_driver == 0) 1116 ) { 1117 1118 switch(nondet_int()) { 1119 1120 case 0: { 1121 1122 /** STRUCT: struct type: usb_driver, struct name: imon_driver **/ 1123 if(ldv_s_imon_driver_usb_driver==0) { 1124 1125 /* content: static int imon_probe(struct usb_interface *interface, const struct usb_device_id *id)*/ 1126 /* LDV_COMMENT_BEGIN_PREP */ 1127 #define pr_fmt(fmt) KBUILD_MODNAME ": " fmt 1128 #define MOD_AUTHOR "Venky Raju <dev@venky.ws>" 1129 #define MOD_DESC "Driver for SoundGraph iMON MultiMedia IR/Display" 1130 #define MOD_NAME "lirc_imon" 1131 #define MOD_VERSION "0.8" 1132 #define DISPLAY_MINOR_BASE 144 1133 #define DEVICE_NAME "lcd%d" 1134 #define BUF_CHUNK_SIZE 4 1135 #define BUF_SIZE 128 1136 #define BIT_DURATION 250 1137 #define IMON_DATA_BUF_SZ 35 1138 /* LDV_COMMENT_END_PREP */ 1139 /* LDV_COMMENT_FUNCTION_CALL Function from field "probe" from driver structure with callbacks "imon_driver". Standart function test for correct return result. */ 1140 res_imon_probe_12 = imon_probe( var_group1, var_imon_probe_12_p1); 1141 ldv_check_return_value(res_imon_probe_12); 1142 ldv_check_return_value_probe(res_imon_probe_12); 1143 if(res_imon_probe_12) 1144 goto ldv_module_exit; 1145 ldv_s_imon_driver_usb_driver++; 1146 1147 } 1148 1149 } 1150 1151 break; 1152 case 1: { 1153 1154 /** STRUCT: struct type: usb_driver, struct name: imon_driver **/ 1155 if(ldv_s_imon_driver_usb_driver==1) { 1156 1157 /* content: static int imon_suspend(struct usb_interface *intf, pm_message_t message)*/ 1158 /* LDV_COMMENT_BEGIN_PREP */ 1159 #define pr_fmt(fmt) KBUILD_MODNAME ": " fmt 1160 #define MOD_AUTHOR "Venky Raju <dev@venky.ws>" 1161 #define MOD_DESC "Driver for SoundGraph iMON MultiMedia IR/Display" 1162 #define MOD_NAME "lirc_imon" 1163 #define MOD_VERSION "0.8" 1164 #define DISPLAY_MINOR_BASE 144 1165 #define DEVICE_NAME "lcd%d" 1166 #define BUF_CHUNK_SIZE 4 1167 #define BUF_SIZE 128 1168 #define BIT_DURATION 250 1169 #define IMON_DATA_BUF_SZ 35 1170 /* LDV_COMMENT_END_PREP */ 1171 /* LDV_COMMENT_FUNCTION_CALL Function from field "suspend" from driver structure with callbacks "imon_driver" */ 1172 ldv_handler_precall(); 1173 imon_suspend( var_group1, var_imon_suspend_14_p1); 1174 ldv_s_imon_driver_usb_driver++; 1175 1176 } 1177 1178 } 1179 1180 break; 1181 case 2: { 1182 1183 /** STRUCT: struct type: usb_driver, struct name: imon_driver **/ 1184 if(ldv_s_imon_driver_usb_driver==2) { 1185 1186 /* content: static int imon_resume(struct usb_interface *intf)*/ 1187 /* LDV_COMMENT_BEGIN_PREP */ 1188 #define pr_fmt(fmt) KBUILD_MODNAME ": " fmt 1189 #define MOD_AUTHOR "Venky Raju <dev@venky.ws>" 1190 #define MOD_DESC "Driver for SoundGraph iMON MultiMedia IR/Display" 1191 #define MOD_NAME "lirc_imon" 1192 #define MOD_VERSION "0.8" 1193 #define DISPLAY_MINOR_BASE 144 1194 #define DEVICE_NAME "lcd%d" 1195 #define BUF_CHUNK_SIZE 4 1196 #define BUF_SIZE 128 1197 #define BIT_DURATION 250 1198 #define IMON_DATA_BUF_SZ 35 1199 /* LDV_COMMENT_END_PREP */ 1200 /* LDV_COMMENT_FUNCTION_CALL Function from field "resume" from driver structure with callbacks "imon_driver" */ 1201 ldv_handler_precall(); 1202 imon_resume( var_group1); 1203 ldv_s_imon_driver_usb_driver++; 1204 1205 } 1206 1207 } 1208 1209 break; 1210 case 3: { 1211 1212 /** STRUCT: struct type: usb_driver, struct name: imon_driver **/ 1213 if(ldv_s_imon_driver_usb_driver==3) { 1214 1215 /* content: static void imon_disconnect(struct usb_interface *interface)*/ 1216 /* LDV_COMMENT_BEGIN_PREP */ 1217 #define pr_fmt(fmt) KBUILD_MODNAME ": " fmt 1218 #define MOD_AUTHOR "Venky Raju <dev@venky.ws>" 1219 #define MOD_DESC "Driver for SoundGraph iMON MultiMedia IR/Display" 1220 #define MOD_NAME "lirc_imon" 1221 #define MOD_VERSION "0.8" 1222 #define DISPLAY_MINOR_BASE 144 1223 #define DEVICE_NAME "lcd%d" 1224 #define BUF_CHUNK_SIZE 4 1225 #define BUF_SIZE 128 1226 #define BIT_DURATION 250 1227 #define IMON_DATA_BUF_SZ 35 1228 /* LDV_COMMENT_END_PREP */ 1229 /* LDV_COMMENT_FUNCTION_CALL Function from field "disconnect" from driver structure with callbacks "imon_driver" */ 1230 ldv_handler_precall(); 1231 imon_disconnect( var_group1); 1232 ldv_s_imon_driver_usb_driver=0; 1233 1234 } 1235 1236 } 1237 1238 break; 1239 default: break; 1240 1241 } 1242 1243 } 1244 1245 ldv_module_exit: 1246 1247 /* LDV_COMMENT_FUNCTION_CALL Checks that all resources and locks are correctly released before the driver will be unloaded. */ 1248 ldv_final: ldv_check_final_state(); 1249 1250 /* LDV_COMMENT_END_FUNCTION_CALL_SECTION */ 1251 return; 1252 1253 } 1254 #endif 1255 1256 /* LDV_COMMENT_END_MAIN */

Here is an explanation of a rule violation arisen while checking your driver against a corresponding kernel.

Note that it may be false positive, i.e. there isn't a real error indeed. Please analyze a given error trace and related source code to understand whether there is an error in your driver.

Error trace column contains a path on which the given rule is violated. You can expand/collapse some entity classes by clicking on corresponding checkboxes in a main menu or in an advanced Others menu. Also you can expand/collapse each particular entity by clicking on +/-. In hovering on some entities you can see some tips. Also the error trace is bound with related source code. Line numbers may be shown as links on the left. You can click on them to open corresponding lines in source code.

Source code column contains a content of files related with the error trace. There is source code of your driver (note that there are some LDV modifications at the end), kernel headers and rule model. Tabs show a currently opened file and other available files. In hovering on them you can see full file names. On clicking a corresponding file content will be shown.

Ядро Модуль Правило Верификатор Вердикт Статус Время создания Описание проблемы
linux-4.3-rc1.tar.xz drivers/staging/media/lirc/lirc_imon.ko 32_7a CPAchecker Bug Fixed 2015-11-14 21:22:22 L0214

Комментарий

reported: 14 Nov 2015

[В начало]