// Skip function: __VERIFIER_error // Skip function: __VERIFIER_nondet_int // Skip function: __VERIFIER_nondet_ulong // Function: __netdev_alloc_skb // with type: struct sk_buff *__netdev_alloc_skb(struct net_device *, unsigned int, gfp_t ) // with return type: (struct sk_buff)* struct sk_buff *__netdev_alloc_skb(struct net_device *arg0, unsigned int arg1, gfp_t arg2) { // Pointer type struct sk_buff *skb = ldv_malloc(sizeof(struct sk_buff)); if(skb) { skb->dev = arg0; skb->head = ldv_malloc(arg1); skb->data = skb->head; skb->tail = 0; } return skb; } // Skip function: calloc // Function: dvb_usb_device_exit // with type: void dvb_usb_device_exit(struct usb_interface *) // with return type: void void dvb_usb_device_exit(struct usb_interface *arg0) { // Void type return; } // Function: dvb_usb_device_init // with type: int dvb_usb_device_init(struct usb_interface *, struct dvb_usb_device_properties *, struct module *, struct dvb_usb_device **, short *) // with return type: int int __VERIFIER_nondet_int(void); int dvb_usb_device_init(struct usb_interface *arg0, struct dvb_usb_device_properties *arg1, struct module *arg2, struct dvb_usb_device **arg3, short *arg4) { // Simple type return __VERIFIER_nondet_int(); } // Skip function: kfree // Function: kmem_cache_alloc // with type: void *kmem_cache_alloc(struct kmem_cache *, gfp_t ) // with return type: (void)* void *kmem_cache_alloc(struct kmem_cache *arg0, gfp_t arg1) { // Pointer type return ldv_malloc(0UL); } // Function: ldv_check_final_state // with type: void ldv_check_final_state() // with return type: void void ldv_check_final_state() { // Void type return; } // Function: ldv_initialize // with type: void ldv_initialize() // with return type: void void ldv_initialize() { // Void type return; } // Function: ldv_probe_3 // with type: int ldv_probe_3() // with return type: int int __VERIFIER_nondet_int(void); int ldv_probe_3() { // Simple type return __VERIFIER_nondet_int(); } // Function: ldv_release_3 // with type: int ldv_release_3() // with return type: int int __VERIFIER_nondet_int(void); int ldv_release_3() { // Simple type return __VERIFIER_nondet_int(); } // Function: ldv_setup_1 // with type: int ldv_setup_1() // with return type: int int __VERIFIER_nondet_int(void); int ldv_setup_1() { // Simple type return __VERIFIER_nondet_int(); } // Function: ldv_some_page // with type: struct page___0 *ldv_some_page() // with return type: (struct page___0)* struct page___0 *ldv_some_page() { // Pointer type return ldv_malloc(sizeof(struct page___0)); } // Skip function: malloc // Skip function: memcpy // Function: msleep // with type: void msleep(unsigned int) // with return type: void void msleep(unsigned int arg0) { // Void type return; } // Function: mutex_lock_interruptible_nested // with type: int mutex_lock_interruptible_nested(struct mutex *, unsigned int) // with return type: int int __VERIFIER_nondet_int(void); int mutex_lock_interruptible_nested(struct mutex *arg0, unsigned int arg1) { // Simple type return __VERIFIER_nondet_int(); } // 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(); } // Function: pskb_expand_head // with type: int pskb_expand_head(struct sk_buff *, int, int, gfp_t ) // with return type: int int __VERIFIER_nondet_int(void); int pskb_expand_head(struct sk_buff *arg0, int arg1, int arg2, gfp_t arg3) { // Simple type return __VERIFIER_nondet_int(); } // Function: skb_clone // with type: struct sk_buff *skb_clone(struct sk_buff *, gfp_t ) // with return type: (struct sk_buff)* struct sk_buff *skb_clone(struct sk_buff *arg0, gfp_t arg1) { // Pointer type return ldv_malloc(sizeof(struct sk_buff)); } // Function: skb_copy // with type: struct sk_buff *skb_copy(const struct sk_buff *, gfp_t ) // with return type: (struct sk_buff)* struct sk_buff *skb_copy(const struct sk_buff *arg0, gfp_t arg1) { // Pointer type return ldv_malloc(sizeof(struct sk_buff)); } // 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_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(); }