// Skip function: __VERIFIER_error // Skip function: __VERIFIER_nondet_int // Skip function: __VERIFIER_nondet_size_t // 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(); } // Skip function: kfree // Function: kzfree // with type: void kzfree(const void *) // with return type: void void kzfree(const void *arg0) { // Void type return; } // Function: ldv_initialize // with type: void ldv_initialize() // with return type: void void ldv_initialize() { // Void type return; } // Skip function: malloc // Skip function: memset // Function: scnprintf // with type: int scnprintf(char *, size_t , const char *, ...) // with return type: int int __VERIFIER_nondet_int(void); int scnprintf(char *arg0, size_t arg1, const char *arg2, ...) { // Simple type return __VERIFIER_nondet_int(); } // Skip function: sscanf // 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: sysfs_create_group // with type: int sysfs_create_group(struct kobject *, const struct attribute_group *) // with return type: int int __VERIFIER_nondet_int(void); int sysfs_create_group(struct kobject *arg0, const struct attribute_group *arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: sysfs_remove_group // with type: void sysfs_remove_group(struct kobject *, const struct attribute_group *) // with return type: void void sysfs_remove_group(struct kobject *arg0, const struct attribute_group *arg1) { // Void type return; } // 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_get_intf // with type: struct usb_interface *usb_get_intf(struct usb_interface *) // with return type: (struct usb_interface)* struct usb_interface *usb_get_intf(struct usb_interface *arg0) { // Pointer type return ldv_malloc(sizeof(struct usb_interface)); } // 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(); }