// Skip function: __VERIFIER_error // Skip function: __VERIFIER_nondet_int // Skip function: __VERIFIER_nondet_ulong // Function: __alloc_pages_nodemask // with type: struct page *__alloc_pages_nodemask(gfp_t , unsigned int, struct zonelist *, nodemask_t *) // with return type: (struct page)* struct page *__alloc_pages_nodemask(gfp_t arg0, unsigned int arg1, struct zonelist *arg2, nodemask_t *arg3) { // Pointer type return ldv_malloc(sizeof(struct page)); } // 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(); } // 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; } // Function: __netif_schedule // with type: void __netif_schedule(struct Qdisc *) // with return type: void void __netif_schedule(struct Qdisc *arg0) { // Void type return; } // Function: __phys_addr // with type: unsigned long int __phys_addr(unsigned long) // with return type: unsigned long int unsigned long __VERIFIER_nondet_ulong(void); unsigned long int __phys_addr(unsigned long arg0) { // Simple type return __VERIFIER_nondet_ulong(); } // Function: __raw_spin_lock_init // with type: void __raw_spin_lock_init(raw_spinlock_t *, const char *, struct lock_class_key *) // with return type: void void __raw_spin_lock_init(raw_spinlock_t *arg0, const char *arg1, struct lock_class_key *arg2) { // Void type return; } // Function: _raw_spin_lock // with type: void _raw_spin_lock(raw_spinlock_t *) // with return type: void void _raw_spin_lock(raw_spinlock_t *arg0) { // Void type return; } // Function: _raw_spin_lock_irqsave // with type: unsigned long int _raw_spin_lock_irqsave(raw_spinlock_t *) // with return type: unsigned long int unsigned long __VERIFIER_nondet_ulong(void); unsigned long int _raw_spin_lock_irqsave(raw_spinlock_t *arg0) { // Simple type return __VERIFIER_nondet_ulong(); } // Function: _raw_spin_unlock // with type: void _raw_spin_unlock(raw_spinlock_t *) // with return type: void void _raw_spin_unlock(raw_spinlock_t *arg0) { // Void type return; } // Function: _raw_spin_unlock_irqrestore // with type: void _raw_spin_unlock_irqrestore(raw_spinlock_t *, unsigned long) // with return type: void void _raw_spin_unlock_irqrestore(raw_spinlock_t *arg0, unsigned long arg1) { // Void type return; } // Function: alloc_netdev_mqs // with type: struct net_device *alloc_netdev_mqs(int, const char *, void (*)(struct net_device *), unsigned int, unsigned int) // with return type: (struct net_device)* struct net_device *alloc_netdev_mqs(int arg0, const char *arg1, void (*arg2)(struct net_device *), unsigned int arg3, unsigned int arg4) { // Pointer type return ldv_malloc(sizeof(struct net_device)); } // Skip function: calloc // Function: consume_skb // with type: void consume_skb(struct sk_buff *) // with return type: void void consume_skb(struct sk_buff *arg0) { // Void type return; } // Function: dev_kfree_skb_any // with type: void dev_kfree_skb_any(struct sk_buff *) // with return type: void void dev_kfree_skb_any(struct sk_buff *arg0) { // Void type return; } // Function: free_netdev // with type: void free_netdev(struct net_device *) // with return type: void void free_netdev(struct net_device *arg0) { // Void type return; } // Function: ldv_initialize // with type: void ldv_initialize() // with return type: void void ldv_initialize() { // Void type return; } // Function: ldv_ndo_init_2 // with type: int ldv_ndo_init_2() // with return type: int int __VERIFIER_nondet_int(void); int ldv_ndo_init_2() { // Simple type return __VERIFIER_nondet_int(); } // Function: ldv_ndo_uninit_2 // with type: int ldv_ndo_uninit_2() // with return type: int int __VERIFIER_nondet_int(void); int ldv_ndo_uninit_2() { // Simple type return __VERIFIER_nondet_int(); } // Skip function: malloc // Skip function: memcpy // Skip function: memset // Function: netif_rx // with type: int netif_rx(struct sk_buff *) // with return type: int int __VERIFIER_nondet_int(void); int netif_rx(struct sk_buff *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: netpoll_trap // with type: int netpoll_trap() // with return type: int int __VERIFIER_nondet_int(void); int netpoll_trap() { // Simple type return __VERIFIER_nondet_int(); } // 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: put_page // with type: void put_page(struct page *) // with return type: void void put_page(struct page *arg0) { // Void type return; } // Function: register_netdev // with type: int register_netdev(struct net_device *) // with return type: int int __VERIFIER_nondet_int(void); int register_netdev(struct net_device *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: skb_add_rx_frag // with type: void skb_add_rx_frag(struct sk_buff *, int, struct page *, int, int, unsigned int) // with return type: void void skb_add_rx_frag(struct sk_buff *arg0, int arg1, struct page *arg2, int arg3, int arg4, unsigned int arg5) { // Void type return; } // Function: skb_put // with type: unsigned char *skb_put(struct sk_buff *, unsigned int) // with return type: (unsigned char)* unsigned char *skb_put(struct sk_buff *arg0, unsigned int arg1) { unsigned char *ret_val = arg0->data + arg0->tail; // a more precise implementation of skb_put would actually re-allocate memory // here arg0->tail += arg1; // Pointer type return ret_val; } // Function: unregister_netdev // with type: void unregister_netdev(struct net_device *) // with return type: void void unregister_netdev(struct net_device *arg0) { // Void type return; } // 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_driver_claim_interface // with type: int usb_driver_claim_interface(struct usb_driver *, struct usb_interface *, void *) // with return type: int int __VERIFIER_nondet_int(void); int usb_driver_claim_interface(struct usb_driver *arg0, struct usb_interface *arg1, void *arg2) { // Simple type return __VERIFIER_nondet_int(); } // Function: usb_driver_release_interface // with type: void usb_driver_release_interface(struct usb_driver *, struct usb_interface *) // with return type: void void usb_driver_release_interface(struct usb_driver *arg0, struct usb_interface *arg1) { // Void type return; } // Function: usb_ifnum_to_if // with type: struct usb_interface *usb_ifnum_to_if(const struct usb_device *, unsigned int) // with return type: (struct usb_interface)* struct usb_interface *usb_ifnum_to_if(const struct usb_device *arg0, unsigned int arg1) { // Pointer type return ldv_malloc(sizeof(struct usb_interface)); } // 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(); } // Function: usb_set_interface // with type: int usb_set_interface(struct usb_device *, int, int) // with return type: int int __VERIFIER_nondet_int(void); int usb_set_interface(struct usb_device *arg0, int arg1, int arg2) { // Simple type return __VERIFIER_nondet_int(); } // Function: warn_slowpath_null // with type: void warn_slowpath_null(const char *, const int) // with return type: void void warn_slowpath_null(const char *arg0, const int arg1) { // Void type return; }