// Skip function: __VERIFIER_error // Skip function: __VERIFIER_nondet_int // Skip function: __VERIFIER_nondet_ulong // Function: __const_udelay // with type: void __const_udelay(unsigned long) // with return type: void void __const_udelay(unsigned long arg0) { // Void type return; } // Function: __dev_kfree_skb_any // with type: void __dev_kfree_skb_any(struct sk_buff *, enum skb_free_reason ) // with return type: void void __dev_kfree_skb_any(struct sk_buff *arg0, enum skb_free_reason arg1) { // Void type return; } // Function: __dynamic_netdev_dbg // with type: int __dynamic_netdev_dbg(struct _ddebug *, const struct net_device *, const char *, ...) // with return type: int int __VERIFIER_nondet_int(void); int __dynamic_netdev_dbg(struct _ddebug *arg0, const struct net_device *arg1, const char *arg2, ...) { // Simple type return __VERIFIER_nondet_int(); } // Function: __netif_schedule // with type: void __netif_schedule(struct Qdisc *) // with return type: void void __netif_schedule(struct Qdisc *arg0) { // Void type return; } // 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)); } // Function: bitrev32 // with type: u32 bitrev32(u32 ) // with return type: u32 unsigned int __VERIFIER_nondet_uint(void); u32 bitrev32(u32 arg0) { // Typedef type // Real type: unsigned int // Simple type return __VERIFIER_nondet_uint(); } // Skip function: calloc // Function: crc32_le // with type: u32 crc32_le(u32 , const unsigned char *, size_t ) // with return type: u32 unsigned int __VERIFIER_nondet_uint(void); u32 crc32_le(u32 arg0, const unsigned char *arg1, size_t arg2) { // Typedef type // Real type: unsigned int // Simple type return __VERIFIER_nondet_uint(); } // Function: dev_trans_start // with type: unsigned long int dev_trans_start(struct net_device *) // with return type: unsigned long int unsigned long __VERIFIER_nondet_ulong(void); unsigned long int dev_trans_start(struct net_device *arg0) { // Simple type return __VERIFIER_nondet_ulong(); } // Function: disable_irq // with type: void disable_irq(unsigned int) // with return type: void void disable_irq(unsigned int arg0) { // Void type return; } // Function: disable_irq_nosync // with type: void disable_irq_nosync(unsigned int) // with return type: void void disable_irq_nosync(unsigned int arg0) { // Void type return; } // Function: enable_irq // with type: void enable_irq(unsigned int) // with return type: void void enable_irq(unsigned int arg0) { // Void type return; } // 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: ether_setup // with type: void ether_setup(struct net_device *) // with return type: void void ether_setup(struct net_device *arg0) { // Void type return; } // Function: ldv_ndo_init_1 // with type: int ldv_ndo_init_1() // with return type: int int __VERIFIER_nondet_int(void); int ldv_ndo_init_1() { // Simple type return __VERIFIER_nondet_int(); } // 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_1 // with type: int ldv_ndo_uninit_1() // with return type: int int __VERIFIER_nondet_int(void); int ldv_ndo_uninit_1() { // 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: memset // Function: netdev_err // with type: int netdev_err(const struct net_device *, const char *, ...) // with return type: int int __VERIFIER_nondet_int(void); int netdev_err(const struct net_device *arg0, const char *arg1, ...) { // Simple type return __VERIFIER_nondet_int(); } // Function: netdev_notice // with type: int netdev_notice(const struct net_device *, const char *, ...) // with return type: int int __VERIFIER_nondet_int(void); int netdev_notice(const struct net_device *arg0, const char *arg1, ...) { // Simple type return __VERIFIER_nondet_int(); } // Function: netdev_warn // with type: int netdev_warn(const struct net_device *, const char *, ...) // with return type: int int __VERIFIER_nondet_int(void); int netdev_warn(const struct net_device *arg0, const char *arg1, ...) { // 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: skb_clone_tx_timestamp // with type: void skb_clone_tx_timestamp(struct sk_buff *) // with return type: void void skb_clone_tx_timestamp(struct sk_buff *arg0) { // Void type return; } // Function: skb_defer_rx_timestamp // with type: bool skb_defer_rx_timestamp(struct sk_buff *) // with return type: bool bool __VERIFIER_nondet_bool(void); bool skb_defer_rx_timestamp(struct sk_buff *arg0) { // Typedef type // Real type: _Bool // Simple type return __VERIFIER_nondet_bool(); } // 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: skb_tstamp_tx // with type: void skb_tstamp_tx(struct sk_buff *, struct skb_shared_hwtstamps *) // with return type: void void skb_tstamp_tx(struct sk_buff *arg0, struct skb_shared_hwtstamps *arg1) { // Void type return; } // Function: trace_hardirqs_off // with type: void trace_hardirqs_off() // with return type: void void trace_hardirqs_off() { // Void type return; } // Function: trace_hardirqs_on // with type: void trace_hardirqs_on() // with return type: void void trace_hardirqs_on() { // Void type return; } // 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; }