// Skip function: __VERIFIER_error // Skip function: __VERIFIER_nondet_int // Skip function: __VERIFIER_nondet_ulong // Function: __dynamic_dev_dbg // with type: int __dynamic_dev_dbg(struct _ddebug *, const struct device *, const char *, ...) // with return type: int int __VERIFIER_nondet_int(void); int __dynamic_dev_dbg(struct _ddebug *arg0, const struct device *arg1, const char *arg2, ...) { // Simple type return __VERIFIER_nondet_int(); } // Skip function: calloc // Function: dev_err // with type: int dev_err(const struct device *, const char *, ...) // with return type: int int __VERIFIER_nondet_int(void); int dev_err(const struct device *arg0, const char *arg1, ...) { // Simple type return __VERIFIER_nondet_int(); } // Function: dev_get_drvdata // with type: void *dev_get_drvdata(const struct device *) // with return type: (void)* void *dev_get_drvdata(const struct device *arg0) { // Pointer type return ldv_malloc(0UL); } // Function: dev_set_drvdata // with type: int dev_set_drvdata(struct device *, void *) // with return type: int int __VERIFIER_nondet_int(void); int dev_set_drvdata(struct device *arg0, void *arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: input_event // with type: void input_event(struct input_dev *, unsigned int, unsigned int, int) // with return type: void void input_event(struct input_dev *arg0, unsigned int arg1, unsigned int arg2, int arg3) { // Void type return; } // Function: input_free_device // with type: void input_free_device(struct input_dev *) // with return type: void void input_free_device(struct input_dev *arg0) { // Void type return; } // Function: input_register_device // with type: int input_register_device(struct input_dev *) // with return type: int int __VERIFIER_nondet_int(void); int input_register_device(struct input_dev *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: input_set_abs_params // with type: void input_set_abs_params(struct input_dev *, unsigned int, int, int, int, int) // with return type: void void input_set_abs_params(struct input_dev *arg0, unsigned int arg1, int arg2, int arg3, int arg4, int arg5) { // Void type return; } // Function: input_unregister_device // with type: void input_unregister_device(struct input_dev *) // with return type: void void input_unregister_device(struct input_dev *arg0) { // Void type return; } // Skip function: kfree // Function: kmemdup // with type: void *kmemdup(const void *, size_t , gfp_t ) // with return type: (void)* void *kmemdup(const void *arg0, size_t arg1, gfp_t arg2) { // Pointer type return ldv_malloc(0UL); } // Function: kstrdup // with type: char *kstrdup(const char *, gfp_t ) // with return type: (char)* char *kstrdup(const char *arg0, gfp_t arg1) { // Pointer type return ldv_malloc(sizeof(char)); } // Function: ldv_initialize // with type: void ldv_initialize() // with return type: void void ldv_initialize() { // Void type return; } // Skip function: malloc // Skip function: memcpy // Skip function: memset // Function: msleep // with type: void msleep(unsigned int) // with return type: void void msleep(unsigned int arg0) { // Void type return; } // Function: mutex_lock_nested // with type: void mutex_lock_nested(struct mutex *, unsigned int) // with return type: void void mutex_lock_nested(struct mutex *arg0, unsigned int arg1) { // Void type return; } // Function: mutex_unlock // with type: void mutex_unlock(struct mutex *) // with return type: void void mutex_unlock(struct mutex *arg0) { // Void type return; } // Function: printk // with type: int printk(const char *, ...) // with return type: int int __VERIFIER_nondet_int(void); int printk(const char *arg0, ...) { // Simple type return __VERIFIER_nondet_int(); } // Skip function: snprintf // Function: strlcat // with type: size_t strlcat(char *, const char *, __kernel_size_t ) // with return type: size_t unsigned long __VERIFIER_nondet_ulong(void); size_t strlcat(char *arg0, const char *arg1, __kernel_size_t arg2) { // Typedef type // Real type: __kernel_size_t // Typedef type // Real type: __kernel_ulong_t // Typedef type // Real type: unsigned long // Simple type return __VERIFIER_nondet_ulong(); } // Function: strlcpy // with type: size_t strlcpy(char *, const char *, size_t ) // with return type: size_t unsigned long __VERIFIER_nondet_ulong(void); size_t strlcpy(char *arg0, const char *arg1, size_t arg2) { // Typedef type // Real type: __kernel_size_t // Typedef type // Real type: __kernel_ulong_t // Typedef type // Real type: unsigned long // Simple type return __VERIFIER_nondet_ulong(); } // Skip function: strlen // Function: usb_alloc_coherent // with type: void *usb_alloc_coherent(struct usb_device *, size_t , gfp_t , dma_addr_t *) // with return type: (void)* void *usb_alloc_coherent(struct usb_device *arg0, size_t arg1, gfp_t arg2, dma_addr_t *arg3) { // Pointer type return ldv_malloc(0UL); } // Function: usb_bulk_msg // with type: int usb_bulk_msg(struct usb_device *, unsigned int, void *, int, int *, int) // with return type: int int __VERIFIER_nondet_int(void); int usb_bulk_msg(struct usb_device *arg0, unsigned int arg1, void *arg2, int arg3, int *arg4, int arg5) { // Simple type return __VERIFIER_nondet_int(); } // Function: usb_control_msg // with type: int usb_control_msg(struct usb_device *, unsigned int, __u8 , __u8 , __u16 , __u16 , void *, __u16 , int) // with return type: int int __VERIFIER_nondet_int(void); int usb_control_msg(struct usb_device *arg0, unsigned int arg1, __u8 arg2, __u8 arg3, __u16 arg4, __u16 arg5, void *arg6, __u16 arg7, int arg8) { // Simple type return __VERIFIER_nondet_int(); } // Function: usb_deregister // with type: void usb_deregister(struct usb_driver *) // with return type: void void usb_deregister(struct usb_driver *arg0) { // Void type return; } // Function: usb_free_coherent // with type: void usb_free_coherent(struct usb_device *, size_t , void *, dma_addr_t ) // with return type: void void usb_free_coherent(struct usb_device *arg0, size_t arg1, void *arg2, dma_addr_t arg3) { // Void type return; } // Function: usb_kill_urb // with type: void usb_kill_urb(struct urb *) // with return type: void void usb_kill_urb(struct urb *arg0) { // Void type return; } // Function: usb_register_driver // with type: int usb_register_driver(struct usb_driver *, struct module *, const char *) // with return type: int int __VERIFIER_nondet_int(void); int usb_register_driver(struct usb_driver *arg0, struct module *arg1, const char *arg2) { // Simple type return __VERIFIER_nondet_int(); }