// Skip function: __VERIFIER_error // Skip function: __VERIFIER_nondet_int // Skip function: __VERIFIER_nondet_ulong // Function: __alloc_workqueue_key // with type: struct workqueue_struct *__alloc_workqueue_key(const char *, unsigned int, int, struct lock_class_key *, const char *, ...) // with return type: (struct workqueue_struct)* struct workqueue_struct *__alloc_workqueue_key(const char *arg0, unsigned int arg1, int arg2, struct lock_class_key *arg3, const char *arg4, ...) { // Pointer type return ldv_malloc(0UL); } // Function: __init_work // with type: void __init_work(struct work_struct *, int) // with return type: void void __init_work(struct work_struct *arg0, int arg1) { // Void type return; } // Function: __list_add // with type: void __list_add(struct list_head *, struct list_head *, struct list_head *) // with return type: void void __list_add(struct list_head *arg0, struct list_head *arg1, struct list_head *arg2) { // Void type return; } // Function: __netlink_kernel_create // with type: struct sock *__netlink_kernel_create(struct net *, int, struct module *, struct netlink_kernel_cfg *) // with return type: (struct sock)* struct sock *__netlink_kernel_create(struct net *arg0, int arg1, struct module *arg2, struct netlink_kernel_cfg *arg3) { // Pointer type return ldv_malloc(sizeof(struct sock)); } // Function: __nlmsg_put // with type: struct nlmsghdr *__nlmsg_put(struct sk_buff *, u32 , u32 , int, int, int) // with return type: (struct nlmsghdr)* struct nlmsghdr *__nlmsg_put(struct sk_buff *arg0, u32 arg1, u32 arg2, int arg3, int arg4, int arg5) { // Pointer type return ldv_malloc(sizeof(struct nlmsghdr)); } // 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: _dev_info // with type: void _dev_info(const struct device *, const char *, ...) // with return type: void void _dev_info(const struct device *arg0, const char *arg1, ...) { // 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 *, unsigned 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, unsigned char arg2, void (*arg3)(struct net_device *), unsigned int arg4, unsigned int arg5) { // 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: destroy_workqueue // with type: void destroy_workqueue(struct workqueue_struct *) // with return type: void void destroy_workqueue(struct workqueue_struct *arg0) { // Void type return; } // Function: dev_err // with type: void dev_err(const struct device *, const char *, ...) // with return type: void void dev_err(const struct device *arg0, const char *arg1, ...) { // Void type return; } // Function: dev_get_by_index // with type: struct net_device *dev_get_by_index(struct net *, int) // with return type: (struct net_device)* struct net_device *dev_get_by_index(struct net *arg0, int arg1) { // Pointer type return ldv_malloc(sizeof(struct net_device)); } // Function: flush_workqueue // with type: void flush_workqueue(struct workqueue_struct *) // with return type: void void flush_workqueue(struct workqueue_struct *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: get_random_bytes // with type: void get_random_bytes(void *, int) // with return type: void void get_random_bytes(void *arg0, int arg1) { // Void type return; } // Function: init_timer_key // with type: void init_timer_key(struct timer_list *, unsigned int, const char *, struct lock_class_key *) // with return type: void void init_timer_key(struct timer_list *arg0, unsigned int arg1, const char *arg2, struct lock_class_key *arg3) { // Void type return; } // Skip function: kfree // 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_ndo_init_4 // with type: int ldv_ndo_init_4() // with return type: int int __VERIFIER_nondet_int(void); int ldv_ndo_init_4() { // Simple type return __VERIFIER_nondet_int(); } // Function: ldv_ndo_uninit_4 // with type: int ldv_ndo_uninit_4() // with return type: int int __VERIFIER_nondet_int(void); int ldv_ndo_uninit_4() { // Simple type return __VERIFIER_nondet_int(); } // Function: ldv_some_page // with type: struct page *ldv_some_page() // with return type: (struct page)* struct page *ldv_some_page() { // Pointer type return ldv_malloc(sizeof(struct page)); } // Function: list_del // with type: void list_del(struct list_head *) // with return type: void void list_del(struct list_head *arg0) { // Void type return; } // Function: lockdep_init_map // with type: void lockdep_init_map(struct lockdep_map *, const char *, struct lock_class_key *, int) // with return type: void void lockdep_init_map(struct lockdep_map *arg0, const char *arg1, struct lock_class_key *arg2, int arg3) { // Void type return; } // Skip function: malloc // Skip function: memcmp // Skip function: memcpy // Skip function: memset // 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: netdev_err // with type: void netdev_err(const struct net_device *, const char *, ...) // with return type: void void netdev_err(const struct net_device *arg0, const char *arg1, ...) { // Void type return; } // Function: netdev_info // with type: void netdev_info(const struct net_device *, const char *, ...) // with return type: void void netdev_info(const struct net_device *arg0, const char *arg1, ...) { // Void type return; } // Function: netif_carrier_on // with type: void netif_carrier_on(struct net_device *) // with return type: void void netif_carrier_on(struct net_device *arg0) { // Void type return; } // Function: netif_rx_ni // with type: int netif_rx_ni(struct sk_buff *) // with return type: int int __VERIFIER_nondet_int(void); int netif_rx_ni(struct sk_buff *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: netif_tx_wake_queue // with type: void netif_tx_wake_queue(struct netdev_queue *) // with return type: void void netif_tx_wake_queue(struct netdev_queue *arg0) { // Void type return; } // Function: netlink_broadcast // with type: int netlink_broadcast(struct sock *, struct sk_buff *, __u32 , __u32 , gfp_t ) // with return type: int int __VERIFIER_nondet_int(void); int netlink_broadcast(struct sock *arg0, struct sk_buff *arg1, __u32 arg2, __u32 arg3, gfp_t arg4) { // Simple type return __VERIFIER_nondet_int(); } // Function: netlink_has_listeners // with type: int netlink_has_listeners(struct sock *, unsigned int) // with return type: int int __VERIFIER_nondet_int(void); int netlink_has_listeners(struct sock *arg0, unsigned int arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: pm_runtime_set_autosuspend_delay // with type: void pm_runtime_set_autosuspend_delay(struct device *, int) // with return type: void void pm_runtime_set_autosuspend_delay(struct device *arg0, int arg1) { // 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: queue_delayed_work_on // with type: bool queue_delayed_work_on(int, struct workqueue_struct *, struct delayed_work *, unsigned long) // with return type: bool bool __VERIFIER_nondet_bool(void); bool queue_delayed_work_on(int arg0, struct workqueue_struct *arg1, struct delayed_work *arg2, unsigned long arg3) { // Typedef type // Real type: _Bool // Simple type return __VERIFIER_nondet_bool(); } // Function: queue_work_on // with type: bool queue_work_on(int, struct workqueue_struct *, struct work_struct *) // with return type: bool bool __VERIFIER_nondet_bool(void); bool queue_work_on(int arg0, struct workqueue_struct *arg1, struct work_struct *arg2) { // Typedef type // Real type: _Bool // Simple type return __VERIFIER_nondet_bool(); } // 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_pull // with type: unsigned char *skb_pull(struct sk_buff *, unsigned int) // with return type: (unsigned char)* unsigned char *skb_pull(struct sk_buff *arg0, unsigned int arg1) { // Pointer type return ldv_malloc(sizeof(unsigned char)); } // 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: sock_release // with type: void sock_release(struct socket *) // with return type: void void sock_release(struct socket *arg0) { // Void type return; } // Skip function: sprintf // Skip function: sscanf // 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_autopm_get_interface // with type: int usb_autopm_get_interface(struct usb_interface *) // with return type: int int __VERIFIER_nondet_int(void); int usb_autopm_get_interface(struct usb_interface *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: usb_autopm_put_interface // with type: void usb_autopm_put_interface(struct usb_interface *) // with return type: void void usb_autopm_put_interface(struct usb_interface *arg0) { // Void type return; } // 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_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_enable_autosuspend // with type: void usb_enable_autosuspend(struct usb_device *) // with return type: void void usb_enable_autosuspend(struct usb_device *arg0) { // Void type return; } // Function: usb_free_urb // with type: void usb_free_urb(struct urb *) // with return type: void void usb_free_urb(struct urb *arg0) { // Void type return; } // Function: usb_get_dev // with type: struct usb_device *usb_get_dev(struct usb_device *) // with return type: (struct usb_device)* struct usb_device *usb_get_dev(struct usb_device *arg0) { // Pointer type return ldv_malloc(sizeof(struct usb_device)); } // 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_put_dev // with type: void usb_put_dev(struct usb_device *) // with return type: void void usb_put_dev(struct usb_device *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(); }