// Skip function: __VERIFIER_error // Skip function: __VERIFIER_nondet_int // Function: __kmalloc // with type: void *__kmalloc(size_t size, gfp_t flags) // with return type: (void)* void *__kmalloc(size_t arg0, gfp_t arg1) { // Pointer type return ldv_malloc(arg0); } // Function: dev_get_drvdata // with type: void *dev_get_drvdata(const struct device *dev) // 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 *dev, void *data) // 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 *dev, unsigned int type, unsigned int code, int value) // 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 *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_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: ldv_check_return_value // with type: void ldv_check_return_value(int res) // with return type: void void ldv_check_return_value(int arg0) { // Void type return; } // Function: ldv_initialize // with type: void ldv_initialize() // with return type: void void ldv_initialize() { // Void type return; } // Function: ldv_undefined_pointer // with type: void *ldv_undefined_pointer() // with return type: (void)* void *ldv_undefined_pointer() { // Pointer type return ldv_malloc(0UL); } // Function: printk // with type: int printk(const char *fmt, ...) // 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: 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: unsigned long // Simple type return __VERIFIER_nondet_ulong(); } // Skip function: strlen // 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_kill_urb // with type: void usb_kill_urb(struct urb *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(); } // Function: usb_submit_urb // with type: int usb_submit_urb(struct urb *urb, gfp_t mem_flags) // with return type: int int __VERIFIER_nondet_int(void); int usb_submit_urb(struct urb *arg0, gfp_t arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: warn_slowpath_null // with type: void warn_slowpath_null(const char *file, const int line) // with return type: void void warn_slowpath_null(const char *arg0, const int arg1) { // Void type return; }