// Skip function: __VERIFIER_error // Skip function: __VERIFIER_nondet_int // Skip function: __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_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: add_timer // with type: void add_timer(struct timer_list *) // with return type: void void add_timer(struct timer_list *arg0) { // Void type return; } // Function: alloc_etherdev_mqs // with type: struct net_device *alloc_etherdev_mqs(int, unsigned int, unsigned int) // with return type: (struct net_device)* struct net_device *alloc_etherdev_mqs(int arg0, unsigned int arg1, unsigned int arg2) { // 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: del_timer_sync // with type: int del_timer_sync(struct timer_list *) // with return type: int int __VERIFIER_nondet_int(void); int del_timer_sync(struct timer_list *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: eth_change_mtu // with type: int eth_change_mtu(struct net_device *, int) // with return type: int int __VERIFIER_nondet_int(void); int eth_change_mtu(struct net_device *arg0, int arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: eth_mac_addr // with type: int eth_mac_addr(struct net_device *, void *) // with return type: int int __VERIFIER_nondet_int(void); int eth_mac_addr(struct net_device *arg0, void *arg1) { // Simple type return __VERIFIER_nondet_int(); } // Function: eth_type_trans // with type: __be16 eth_type_trans(struct sk_buff *, struct net_device *) // with return type: __be16 unsigned short __VERIFIER_nondet_ushort(void); __be16 eth_type_trans(struct sk_buff *arg0, struct net_device *arg1) { // Typedef type // Real type: __u16 // Typedef type // Real type: unsigned short // Simple type return __VERIFIER_nondet_ushort(); } // Function: eth_validate_addr // with type: int eth_validate_addr(struct net_device *) // with return type: int int __VERIFIER_nondet_int(void); int eth_validate_addr(struct net_device *arg0) { // Simple type return __VERIFIER_nondet_int(); } // Function: free_irq // with type: void free_irq(unsigned int, void *) // with return type: void void free_irq(unsigned int arg0, void *arg1) { // 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_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_3 // with type: int ldv_ndo_init_3() // with return type: int int __VERIFIER_nondet_int(void); int ldv_ndo_init_3() { // Simple type return __VERIFIER_nondet_int(); } // Function: ldv_ndo_uninit_3 // with type: int ldv_ndo_uninit_3() // with return type: int int __VERIFIER_nondet_int(void); int ldv_ndo_uninit_3() { // 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)); } // Skip function: malloc // 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: 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: 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: 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: request_threaded_irq // with type: int request_threaded_irq(unsigned int, irqreturn_t (*)(int, void *), irqreturn_t (*)(int, void *), unsigned long, const char *, void *) // with return type: int int __VERIFIER_nondet_int(void); int request_threaded_irq(unsigned int arg0, irqreturn_t (*arg1)(int, void *), irqreturn_t (*arg2)(int, void *), unsigned long arg3, const char *arg4, void *arg5) { // Simple type return __VERIFIER_nondet_int(); } // 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; }